It is also interesting that there are many parallels between software engineering and the design of mathematical proofs (or theoretical CS proofs, which I am mo

It is also interesting that there are many parallels between software engineering and the design of mathematical proofs (or theoretical CS proofs, which I am more familiar with). In theoretical CS, people talk of catching and fixing "bugs" in proofs, namely, mistakes that make the proof fail but can hopefully be fixed while sticking to essentially the same idea. One can "refactor" proofs, in superficial ways (e.g., renaming of concepts), but in deeper ways also, e.g., extract part of a proof to make it an independent lemma that you can reuse (or "invoke") from other parts of the proof. One often tries to "decouple" large proofs into independent parts with clearly defined "interfaces", that the reader can understand separately from each other, though this usually implies a tradeoff (a more tightly integrated proof requires more mental space but is usually shorter overall). One can think of the statement of sub-results (lemmas) as providing an "interface" to invoke them elsewhere, which you try to "decouple" from the actual "implementation", namely, the way the lemmas are really proven. It takes practice to find the right way to abstract away the essence of a result to state it correctly, without burdening it with implementation details, but without forgetting an important aspect of the result that will be necessary later. As in software engineering, once a result is proven, you stop burdening your mind with the implementation and mostly think about the statement (i.e., what the result is supposed to be doing) when using it. In software engineering, one must decide which part of the code is "responsible" for checking certain properties on the objects, and that code may "assume" some preconditions on its inputs and must "guarantee" some preconditions on its outputs. In the same way, in proofs, one often wonders where certain conditions should be verified. Should they be part of the definition of the object? Does this lemma enforce more conditions on the object than what is guaranteed by its statement? The parallel is not perfect. In software engineering, you can rely on the computer to check that your code is correct, and to execute it. In mathematics you rely on other humans to do this and check that they are convinced by your proofs. This means you can get away with appeals to human intuition which are not fully formal, but on the other hand there is no safety net when you make an error in your reasoning, no reality check that you can invoke to avoid exploring erroneous consequences. Also, this does not apply to all types of proofs; but it applies especially well to proofs that describe a construction, i.e., a way to "build" a certain abstract object, often to justify that an object with a certain desirable set of properties exists.