Curry-Howard Isomorphism

This is an observation that the simply-typed lambda calculus and intuitionistic propositional logic correspond, or in a nutshell:

Types are logical formulas.
A term of a type is a proof of that type's formula.
Evaluation corresponds to proof resolution.

Let's put it simply. If a program exists that accepts an integer as an input, and produces a character as an output, then the sentence "If I've an integer, then I also have a character" is (with caveats) true. Written simply this phrase sounds as Int -> Char. The proof of this sentence is, precisely, the existence of the program. All the programs that consume an integer and produce a character are proofs of this sentence. Of course, a program is constructed by composing some elementary programs, the instructions, which are assumed as basic building blocks given a priori. This building blocks are our axioms, and the procedure to assemble them is, by its very nature, constructive. The nice thing is that the analogy can be reversed: If I create a novel logic, and I define for it a constructive (whatever the word means) proof system for it, then I can regard the proof system as a novel programming language.

There are many online documents in postscript on this. Here is one introduction as a plain web page.

This page is linked from: Basic Computer Science Coq Logic