What is the Difference Between Proofs and Programs?

Curry and Howard observed that ordinary propositional logic can also be viewed as a functional (programming) language. Thus programs are contained, in a certain sense, in proofs in mathematical logic. The underlying reason (in the present author's view) is because of the formal, that is to say, purely syntactic, similarities between logical rules and those of the lambda calculus. This has led to the viewing of proofs (originally, just in formal logic) as computer programs. The advantage of these techniques is that the task of programming a function is reduced to reasoning with domain knowledge. In this paper we sketch the development of the Curry-Howard correspondence, first of all into predicate calculus, then into arithmetic. After that we look at different applications of the idea of the Curry-Howard process into two very different applications: algebraic specifications and imperative programming. The full details may be found in our forthcoming book with Iman Poernomo and Martin Wirsing. Finally, having seen how proofs may be said to contain programs, we discuss the question of whether there are, or should be, proofs in programs.