HackerTube.dev

"Propositions as Types" by Philip Wadler

Strange Loop Conference · 143.6K views · 2015-09-26 · 42:43

Open on YouTube ↗

If playback is restricted in your region, try opening the original video. Use Mark watched to add it to your marked videos.

Overview

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.

On Hacker News

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.

Recommended by 9 HN people across 8 months · HN mentions 2015–2026

Topics

Logic & formal methodsProgramming language designComputability & complexity theory
Search by tags
curry-howardlambda calculustype theoryfunctional programminglogichistory of computing

What people said

jgautsch · 2018-08 · Strong recommendation

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: [VIDEO]

Read the original HN comment ↗
imode · 2017-01 · Strong recommendation

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. * [VIDEO]

Read the original HN comment ↗
runT1ME · 2016-10 · Strong recommendation

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.

Read the original HN comment ↗

Sources

Video by Strange Loop Conference, played through YouTube.

Data and selection notes

HN summaries and labels may contain AI errors. HN dates refer to discussions, not video publication.

HN Library: HackerTube export (2026-10-31) and open-index/hacker-news. Upstream summaries and classifications may contain AI errors.

Views, duration and playback status refresh separately from the published catalog. When an update fails, existing data remains visible.

Selection checks
  • SaaS & AI candidates: Topic keywords do not match
  • Editor-approved picks: Editorial review is required

Rule matches identify candidates. They do not guarantee video quality or financial results.

About the library and its sources