Curry-Howard correspondence

Curry-Howard correspondence is a special property of pCIC, which can construct a correct program from proof, and vice versa.


----wiki has an excellent statement about this----
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

1. the return type of a function (i.e., the type of values returned by a function) is analogous to a logical theorem,
2. subject to hypotheses corresponding to the types of the argument values passed to the function;
3. 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
-------------------------------------------------