From my understanding, most of mathematics can be built up assuming a mechanical procedure of manipulating finite strings of symbols according to certain rules. A conventional way to do it is via the ZFC language of set theory. We can start off with axioms from ZFC and first-order logic, and deduce new theorems according to mechanical procedures. These completely symbolic theorems and proofs can then be translated into natural language (say English). I understand the typical non-formal proof in math to then be a convincing argument that the formal proof can be written in formal symbols.
Now common math objects can be represented as sets (e.g. a function is a set of ordered pairs, which can be represented as sets) and thus we can prove things about them in formal ZFC. However, I've never seen any semblance of an algorithm or its proof written in formal logic. For example, consider the binary search algorithm. How would one write it in the language of ZFC? How would one prove its correctness, termination and "running time" formally (in ZFC) too? Does anyone have an example?