Clean Proofwriting

Recently I have been learning some about agile programming for the first time, mainly by reading Robert C. Martin's Clean Code. I've been struck by how similar writing clean code is to writing readable proofs, so I thought I'd explore the similarities here.

I'll simply go through some of Martin's main points that I think relate to writing mathematical proofs. Note that I do not necessarily agree that proofwriters should go to the extreme of following all these rules for every proof, but many proofs I have read could be improved using these principles.

Meaningful Names

Martin dedicates the chapter after the introduction to explaining the necessity of meaningful names. Of course, this translates to naming definitions of mathematical constructions wisely. Use words that invoke appropriate metaphors, so that the interactions of the mathematical objects defined sound natural, even if the reader has not previously encountered the definition.

Keep Functions (Theorems) Small

Functions, writes Martin, should have a single task. This reduces code redundancy and makes it easier to understand what a function does. The mathematical analog to functions is theorems and lemmas, so using this principle in proofwriting means keeping theorems small, using sequences of small lemmas if necessary. For example, anytime it is necessary to cite "the proof of theorem X", it's a sign that "theorem X" should be split up using lemmas. Unlike giving definitions meaningful names, this is a principle mathematicians often violate. Such violations seem sometimes justified, but not nearly so often as they occur.

Comments and Explanation

Using meaningful names and keeping functions small should make it clear what the code does with minimal comments, and likewise with proofs. But when comments are required to understand what a function or theorem is intended to do, they should be included. Some proof writers appear to believe that brevity is beauty, and if a short proof must be studied and studied to be understood, it only proves the excellence of its author's intelligence. This believe is found in computer programmers too, and indeed many are proud to come up with very short programs to accomplish certain tasks. While brevity often forces beautiful logic, it does not lend itself to explanation. Programmers have recently realized that explanation is necessary in code, for the sake of the next programmer. If explanation is necessary in code, which works as long as the computer can follow the logic, then it is certainly necessary in proofs, of which the only readers are human. To summarize, good names and structure will limit the need for explanation, but necessary explanation should still be included.

I could go on (particularly about translating OOP principles to proofwriting), but I'll stop here. Following these principles in writing proofs will result in many small lemmas and theorems, but each chunk will be more easily understood, and once a theorem or lemma works, it need not be checked again, as the reader proceeds through the paper. This should minimize instances of citing proofs of theorems, or saying that a proof follows similarly to some other proof, or other crutches we depend on when tasked with putting the mathematical structure in our mind's eye down on paper.

comments powered by Disqus