THE VIDEO SHELF · propositions as types
"Propositions as Types" by Philip Wadler
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.
Why HN readers recommended it
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.
This is a summary from the source dataset, not an endorsement by Hacker News or the video creator.
Video & recommendation details
- Creator / channel
- Strange Loop Conference
- Topic
- propositions as types
- Format
- talk
- Level
- intermediate
- HN recommenders in dataset
- 9
- HN mentions in dataset
- 20
- Recommendation years in dataset
- 2015–2026
These counts and years describe the included Hacker News records; they are not YouTube views or the video’s publication date.
From the original HN conversations
Excerpts from the recorded comments. Follow each source for the full comment and surrounding discussion.
+1 Probably my favorite talk at Strange Loop this year. It's worth watching just for the minute or so starting here: [VIDEO]
jcox92 on Hacker News · 2015-11
In Propositions as Types (2014) [pdf]Propositions as Types: [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.
runT1ME on Hacker News · 2016-10
In Ask HN: What's your favorite tech talk?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 …
imode on Hacker News · 2017-01
In Proofs are Programs – 19th Century Logic and 21st Century Computing (2000) [pdf]
Summaries, classifications and recommendation records are from the HackerTube source dataset. Read about this library and its limitations.
