Propositions as Types: Connecting Logic and Computation

The subject of this episode's paper — Propositions as Types by Philip Wadler — is one of those grand ideas that makes you want to go stargazing. To stare out into space and just disassociate from your body and become one with the heavens. Everything — life, space, time, existence — all of it is a joke! A cosmic ribbing delivered by the laws of the universe or some higher power or, perhaps, higher order. Humanity waited two thousand years, from the time of the ancient Greeks through until the 1930s, for a means to answer questions of calculability, when three suddenly arrived all at once:

• General recursive functions by Gödel in 1934, with functions of sets of natural numbers.
• Lambda calculus by Alonzo Church in 1936, with anonymous single-variable functions.
• Turing machines by Alan Turing in 1937, with a process for evaluating symbols on a tape.

Then it was discovered that these three models of computation were, in fact, perfectly equivalent. That any statement made in one could be made in the others. A striking coincidence, sure, but not without precedent. But then it was quietly determined (in 1934, again in 1969, and finally published in 1980) that computation itself is in a direct correspondence with logic. That every proposition in a given logic corresponds with a type in a given programming language, every proof corresponds with a program, and the simplification of the proof corresponds with the evaluation of the program.

The implications boggle the mind. How could this be so? Well, how could it be any other way? Why did it take so long to discover? What other discoveries like this are perched on the precipice of revelation?

Philip Wadler is here to walk us through this bit of history, suggest answers to some of these questions, and point us in a direction to search for more.

And we are here, dear listener, to level with you that a lot of this stuff is miserably hard to approach, presented with the symbols and language of formal logic that is so often inscrutable to outsiders. By walking you through Wadler's paper (and the much more approachable Strange Loop talk), and tying it in with the cultural context of modern functional programming, we hope you'll gain an appreciation for this remarkable, divine pun that sits beneath all of computation.

Links

=> patreon.com/futureofcoding — but only if you back the Visual Programming tier!! I'm warning you!

• Wadler's Strange Loop talk Propositions as Types
• Cocoon is good. It's not, like, Inside or Limbo good, but it's good. Actually, just play Inside. Do that ASAP.
• Hollow Knight, also extremely good. Can't wait for Silksong. But seriously, if you're reading this and have haven't played Inside, just skip this episode of the podcast and go play Inside. It's like 3 hours long and it's, like, transformatively great.
• Chris Martens has done some cool work (eg) bringing together linear logic and games.
• Meh: Gödel, Escher, Bach by Douglas Hofstadter
• Yeh: Infinity and the Mind by Rudy Rucker
• Heh: To Mock a MockingBird by Raymond Smullyan.
• The hierarchy of automata
• Games: Agency as Art
• The Incredible Proof Machine is what some would call a "visual programming language" because proofs are programs. But it's actually really cool and fun to play with. Approach it like a puzzle game, and give it 10 minutes or so to get its hooks into you.
• "Stop Doing Logic" is part of the Stop Doing Math meme. Unrelated: Ivan's song Don't Do Math.
• Bidirectional Type Checking, a talk by David Christiansen
• List Out of Lambda, a blog post by Steve Losh

Nobody noticed that these links were silly last time, so this time I'm drawing more attention to it:

• Ivan: Mastodon • Email
• Jimmy: Mastodon • Twitter

This link is legit:

• DM us in the FoC Slack

https://futureofcoding.org/episodes/068

Support us on Patreon: https://www.patreon.com/futureofcoding

See omnystudio.com/listener for privacy information.