Proving and Programming

Cristian Calude

University of Auckland

Abstract

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 correctness).

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.