hackertube.io

"Propositions as Types" by Philip Wadler

Strange Loop Conference · talk · Watch on YouTube

Logic & formal methodsProgramming language designComputability & complexity theory

What it is

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 Hacker News recommends 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.

  • 9 people recommended it
  • 8 different months
  • 4 strong recommendations
  • first 2015, last 2026

What HN commenters said

  1. “Probably my favorite talk at Strange Loop this year.”

    Favorite talk of the conference

    jcox92, 2015-11 · Strong recommendation · in “Propositions as Types (2014) [pdf]”

  2. “I think this can really really change how we look at everyday programming tasks”

    Changes how you view everyday programming tasks

    runT1ME, 2016-10 · Strong recommendation · in “Ask HN: What's your favorite tech talk?”

  3. “best ~40 minutes I've ever spent.”

    Opened eyes to the utility of logic in everyday programming

    imode, 2017-01 · Strong recommendation · in “Proofs are Programs – 19th Century Logic and 21st Century Computing (2000) [pdf]”

  4. “it's one of my favorite talks. Well worth a watch if you haven't seen it”

    Introduces Curry-Howard correspondence with history and follow-on ideas

    jgautsch, 2018-08 · Strong recommendation · in “Curry–Howard correspondence”

  5. “Philip gave a extremely entertaining talk on the same subject at Strange Loop this year”

    Entertaining talk on the same subject as the paper

    chrislloyd, 2015-11 · Recommendation · in “Propositions as Types (2014) [pdf]”

  6. “If you like watching videos, try”

    Authority on proofs being programs, in video form

    mietek, 2016-07 · Recommendation · in “Very Long Proofs”

  7. “that was the talk that introduced Lambdaman to the world.”

    Favorite tech talk, also introduced Lambdaman

    yawaramin, 2018-04 · Recommendation · in “Ask HN: What is your favourite tech talk?”

  8. “A really in depth look into why functional languages stand out as a programming paradigm.”

    In-depth look at functional languages paralleling mathematical logic

    pmiri, 2018-10 · Recommendation · in “Ask HN: What are some of the best technical talks you've heard?”

Excerpts from Hacker News comments, linked to the originals. Summaries and labels were written by a language model from those comments.

Topics: curry-howard, lambda calculus, type theory, functional programming, logic, history of computing

Also recommended by the same people