Strange Loop Conference
9 HN recommenders · recommended in 19 months, 2015–2026
42:43 · 144K views · Sep 26, 2015
Philip Wadler's Strange Loop talk on Propositions as Types, the link between logic and computation (the Curry-Howard correspondence). He traces its history through Church, Godel and Turing and shows how it shaped theorem provers and programming languages.
HN regards it as an entertaining and eye-opening introduction to why logic and functional programming are connected, and it is a frequent pick in favorite-tech-talk threads.
20 comments from Hacker News
curry-howard and Wadler's "Propositions as Types" talk at StrangeLoop* opened my eyes pretty early on to the sweet, sweet utility of logic in my every day programming. it sounds odd to start with but I never realized why these things mattered prior to viewing this talk. props to wadler. best ~40 minutes I've ever spent. * this video
Professor Philip Wadler has a fantastic talk titled "Propositions as Types" that introduces the Curry-Howard correspondence, some history behind it and ideas following it. In fact it's one of my favorite talks. Well worth a watch if you haven't seen it: this video
Propositions as Types: this video I think this can really really change how we look at everyday programming tasks everywhere from the type of tooling we choose to how we approach problems.
+1 Probably my favorite talk at Strange Loop this year. It's worth watching just for the minute or so starting here: this video
If you’re using the right language, proofs are programs; it’s as simple as that. “Compressing” a proof, then, amounts to doing what good programmers are already doing — noticing patterns and eliminating redundancy. I’ll refer you to an authority on the subject, Phil Wadler. If you like watching videos, try < this video . If you’d rather read an entertaining paper, try < [LINK] .