Proving and Programming
University of Auckland
There is a strong analogy between proving theorems in mathematics and
writing programs in computer science. This paper is devoted to
an analysis, from the perspective of this analogy, of proof in
mathematics. We will argue that:
1. Theorems (in mathematics)
correspond to algorithms and not programs (in computer science);
algorithms are subject to mathematical proofs (for example for
2. The role of proof in mathematical modeling is
very little: adequacy is the main issue.
3. Programs (in
computer science) correspond to mathematical models. They are not subject to proofs, but to an adequacy analysis; in this type of analysis, some proofs may appear. Correctness proofs in computer science (if any) are not cost-effective.
4. Rigor in programming is superior to rigor in mathematical proofs.
5. Programming gives mathematics a new form of understanding.
6. Although the Hilbertian notion of proof has few chances to change, future proofs will be of various types, will play different roles, and their truth will be checked differently.