Computer programs and mathematical proofs are similar in certain ways. Using this similarity, we can develop tools which help both programmers write better programs and mathematicians write better proofs.

There is an analogy between the process of writing programs and the process of proving mathematical theorems. Generally speaking, to write a program, the programmer decides what the program must do, chooses an algorithm, and breaks the algorithm down into small computational steps until the program compiles. To prove a theorem, a mathematician formulates a statement of the theorem, chooses a proof technique, and breaks the argument down into small logical steps until the proof is accepted by other people. In both cases, it is important that the program or proof do what it was intended to do -- either perform some computation or justify some mathematical result.

Notice that one difference is that mathematical proofs are usually written for people, where computer programs are written to be read by a computer. However, if proofs are broken down into very small steps and written in a formal language, it is possible for a computer to recognize a correct proof. Some computer programs can help people develop correct proofs as well as just checking if a particular finished proof is correct.

As well as being tools for mathematicians and other people who need to use careful reasoning, these proof checking/proof building systems can be used to help write computer programs. This is because certain kinds of mathematical proofs actually show how to compute a result -- for example, a proof that every number has a factorization into primes might work by showing how to do the factorization. In that case, the proof would essentially describe a program which calculated prime factors.

This means that a computer system which checks that proofs are correct might also be able to check that programs are correct, and a tool for developing correct proofs could also be used to develop correct programs. (It may seem circular to use a program to write a program, but things like text editors and compilers are programs which enable people to write programs.) Some combined proof and programming tools like this already exist, and computer scientists are working on making these tools easier to use, both for proving mathematical theorems and writing programs.