In the preceding post I linked the regular expressions that define tokens in a programming language to the definitions in a formal mathematical system. Productions of the grammar that define the language, I said, were axioms. The programs we write in that language are theorems.
The definitions and axioms of Euclid's Geometry construct a formal mathematical system. The proof of theorems in geometry "stand on the shoulders" of other theorems. For any theorem there is a "tree" of theorems. The theorem to be proved is the root node of the tree. Definitions and axioms are the leaf nodes. That is how the complete system is constructed.
That is how programs should be constructed. Sure, everyone constructs programs that consist of functions. But do we check the complexity of the functions? We need to refactor till we get functions that have low complexity. Such functions are easy to inspect and easy to test (unit test). If all the functions in the call tree of a function have been "proved" - by inspection and unit test coverage - then the function itself stands on a "proven" foundation.
Programs must be "proven" with rigor approximating the rigor with which geometry theorems are proven. Tools for Complexity metrics, Refactoring, Unit Testing, & Coverage metrics are the instruments that help in doing this.
Earlier post on the subject.
