Wow. The essay they keep referring to throughout the exchange --Wadler's "Proposition and Types" [1]-- is hands down the best exposition of the Curry-Howard cor

Wow. The essay they keep referring to throughout the exchange --Wadler's "Proposition and Types" [1]-- is hands down the best exposition of the Curry-Howard correspondence I've seen so far: deep but thoroughly readable (Howard wasn't just being nice!). Even if you already know this stuff, I seriously recommend reading it (this one, or any of his other expository writings on this topic [2]). His perspective is formidable. [1] http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-... [2] http://homepages.inf.ed.ac.uk/wadler/topics/history.html http://homepages.inf.ed.ac.uk/wadler/topics/history.html