This is an observation that the simply-typed lambda calculus and  intuitionistic propositional *(logic) correspond, or in a nutshell:
<ul>
<li>Types are logical formulas.
<li>A term of a type is a proof of that type's formula.
<li>Evaluation corresponds to proof resolution.
</ul>
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.

<ul class="links">
<li>There are many online documents in postscript on this. Here is _("one introduction"|http://www.cse.psu.edu/~catuscia/teaching/cg520/99Fall/lecture_notes/L11and12.html) as a plain web page.
</ul>
