This is my short summary of Philip Wadler’s Proofs are Programs: 19th Century Logic and 21st Century Computing.

Proofs and programs are the same thing. But it took a century of efforts to recognize the relationship.

• Modern logic began with Gottlob Frege’s Begriffschrift in 1879.
• Gerhard Gentzen introduced natural deduction in 1934.
• Alonzo Church introduced lambda calculus in 1932. He also introduced a typed version of lambda calculus in 1940.
• Dag Prawitz showed how to simplify natural deduction proofs directly in 1956.
• Haskell Curry noted a correspondence between the types of the combinators and the laws of logic as formulated by Hilbert in 1956.
• W. A. Howard put together the results of Curry and Prawitz, and wrote down the correspondence between natural deduction and lambda calculus in 1969.
• Howard’s work was published in 1980.

So it took more than 30 years to recognize the correspondence between Gentzen’s natural deduction and Church’s typed lambda calculus. They are the same thing! Proofs and programs. This correspondence is called Curry-Howard Isomorphism.

Logicians and computer scientists have discovered exactly the same type systems!

• Hindley-Milner type system: Hindley (1969), Milner (1978).
• Girard-Reynolds system: Girard (1972), Reynolds (1974).
• .. still being discovered

A talk by Phil Gossett given in Google’s Advanced Programming Language series is the best explanation of Curry-Howard isomorphism I’ve seen.

He briefly mentioned the origin of type system at the beginning and explained Hindley-Milner, Type Classes (Wadler-Blott), Curry-Howard and Girard-Reynolds. Especially, he showed the relationship between parametricity and Girard-Reynolds isomorphism.

He finished his talk by describing Lennart Augustsson’s Djinn, which is small program that takes a (Haskell) type and gives you back a function of that type if one exists.

In his talk, he gave some examples of Curry-Howard isomorphism.

• Intuitonistic logic <-> Combinatory logic (-> Lambda Calculus)
• Girard representation theorem <-> Reynolds abstraction theorem
• F2 <-> P2

BTW, there are a few technical errors in the talk. Please refer to Wadler’s comment on the talk.