Among the papers that I've read this year, I found "Propositions As Types", by Phillip Wadler to be one of the more interesting. I had to read it a few times, then watch a few talks on it, before it actually sank in. This post is a reprint of a description I emailed to a friend. It’s not often that I get this intellectually excited. The paper’s insights are so revealing that I wanted to share them with whatever audience I have.
Regarding the deep Correspondence between Formal Logic and Programming Languages, Wadler asserts:
- Propositions in a Formal Logic, correspond to Types in a Programming Language
- Proofs in the Logic, correspond to terms, or programs, in the Programming Language
- Simplification of Proofs, corresponds to evaluation of programs
A) Michael Bernstein gives a good interpretation of the ideas in "Propositions as Types".
B) And this is Phillip Wadler's latest talk, given at StrageLoop 2015, on the subject.
C) For extra credit, here Wadler introduces four calculi for gradual typing (what Racket and clojure/core.typed use):
λB, based on the blame calculus of Wadler and Findler (2009)
λC, based on the coercion calculus of Henglein (1994)
λT and λW, based on the three- some calculi with and without blame of Siek and Wadler (2010).
He defines translations from (λB to λC), from (λC to λT), and from (λT to λW).
I've lately thought that Computer Science (or Informatics?) qualifies as an actual science, because data and computation exist in nature. Here, Wadler is asking if programming languages are invented or discovered, which is pretty fascinating to contemplate. Wadler thinks it's the latter, and so do I. If formal logics correspond to programming languages, it's just another piece of evidence in our favour.