If one now abstracts on the peculiarities of this or that formalism, the immediate generalization is the following claim: a proof is a program, the formula it proves is a type for the program. Most informally, this can be seen as an analogy which states that the return type of a function (i.e., the type of values returned by a function) is analogous to a logical theorem, subject to hypotheses corresponding to the types of the argument values passed to the function; and that the program to compute that function is analogous to a proof of that theorem. This sets a form of logic programming on a rigorous foundation: proofs can be represented as programs, and especially as lambda terms, or proofs can be run.

The correspondence has been the starting point of a large spectrum of new research after its discovery, leading in particular to a new class of formal systems designed to act both as a proof system and as a typed functional programming language.

— Wikipedia on Curry–Howard correspondence

2010.03.07 Sunday ACHK