"Propositions as Types" by Philip Wadler
9 人推荐 · 跨 8 个月 · 2015–2026
中文导读
Philip Wadler 在 Strange Loop 上的重磅演讲《Propositions as Types》，系统阐释了连接数理逻辑与计算世界的 Curry-Howard 同构。他顺着 Church、Gödel 到 Turing 的思想脉络，展示了这一理论如何奠定现代定理证明器与编程语言的基石。
为什么 HN 推它
HN 网友公认既风趣幽默又极具启发性的神作，将逻辑与函数式编程的深层关联讲得透彻入骨，经常入选各类最佳技术演讲盘点。
「这是我一生中度过最值得的40分钟。」HN 网友原话：best ~40 minutes I've ever spent.
英文原摘要（HackerTube / Claude 整理）
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.
HN 上的提及
Philip gave a extremely entertaining talk on the same subject at Strange Loop this year
Probably my favorite talk at Strange Loop this year.
If you like watching videos, try
I think this can really really change how we look at everyday programming tasks
claims that aliens will probably have discovered it