Importance Of Geometry

I believe the subject of geometry to be the most important subject taught in schools. It is first rate preparation for the mind for any profession that that requires reasoning. Abraham Lincoln kept a copy of Euclid's Elements of Geometry in his saddlebag, and studied it late at night by lamplight; he related that he said to himself, " … you never can make a lawyer if you do not understand what demonstrate means; and I left my situation in Springfield, went home to my father's house, and stayed there till I could give any proposition in the six books of Euclid at sight. I then found out what demonstrate means, and went back to my law studies" (see The Abraham Lincoln connection.)

A very readable translation of the 13 books of Elements is available here.

Euclid built geometry on ten postulates (axioms). In addition to the axioms, each of the books contains definitions of the geometric terms used in that book and following books. No symbols (as in current geometry textbooks) are used. This make the proofs verbose. The proofs are all graphical as Euclid did not have symbolic algebra that we use today. What he had was Geometrical Algebra. The proof of Pythagoras’s Theorem is an example.

Application of Euclid’s Method to Software

Software should be provably correct. The propositions in Euclid’s books rest on propositions proved earlier. The initial propositions of Book 1 depend just on the definitions and axioms. They are like the leaf functions in a program. I believe that software constructed in the same way will result in provable software.

What a function should do (including any side-effects) should be clearly documented like a proposition. The function body itself is equivalent to a sequence of geometric constructions.

I have found that writing unit tests drives the process of re-factoring code into simpler functions. If unit tests are getting messy, the function under test is messy. The function must be re-factored.

Unit tests and re-factoring are the initial stages. These must be followed by proof of correctness of the construction. The process is not linear; it is cyclical. If the proof is difficult, decompose the function yet again.

A proof answers the question, “Why will this do what it is meant to do?” It should be part of the function documentation. Correctness of the proof must be attested to in the same manner as mathematical proofs. It must be accepted by peers who understand what is being coded.

Assertions, Preconditions, and Post-conditions are akin to lemmas. They are simpler to prove. In addition they have the added advantage of being executable.

Of course, proofs, despite peer reviews, can be defective. That does not mean they should not be attempted. We should learn from defective proofs.