'Propositions as Types' by Philip Wadler

The principle of Propositions as Types links logic to computation. At first sight it appears to be a simple coincidence---almost a pun---but it turns out to be remarkably robust, inspiring the design of theorem provers and programming languages, and continuing to influence the forefronts of computing. Propositions as Types has many names and many origins, and is a notion with depth, breadth, and mystery. Learn why functional programming is (and is not) the universal programming language.

Philip Wadler
UNIVERSITY OF EDINBURGH
@PhilipWadler

Philip Wadler is Professor of Theoretical Computer Science at the University of Edinburgh. He is an ACM Fellow and a Fellow of the Royal Society of Edinburgh, past chair of ACM SIGPLAN, past holder of a Royal Society-Wolfson Research Merit Fellowship, and a winner of the POPL Most Influential Paper Award. Previously, he worked or studied at Stanford, Xerox Parc, CMU, Oxford, Chalmers, Glasgow, Bell Labs, and Avaya Labs, and visited as a guest professor in Copenhagen, Sydney, and Paris. He has an h-index of 60, with more than 18,000 citations to his work according to Google Scholar. He contributed to the designs of Haskell, Java, and XQuery, and is a co-author of Introduction to Functional Programming (Prentice Hall, 1988), XQuery from the Experts (Addison Wesley, 2004) and Generics and Collections in Java (O'Reilly, 2006). He has delivered invited talks in locations ranging from Aizu to Zurich.

[JoshAdams]

This is one of the best talks I've ever watched. If I could just encourage relatively young but hungry programmers to watch one talk, it might be this one. It led to me firing off about 4 different emails just while watching it, all of which I hope have some small impact on people.

[OttoNascarella]

Wadler, Philip - "you don't put science in your name if you're real science"

[estebanmarin]

What a great conference. It's nice to walk that anthropologic path of the people and the context things were discovered. This gives better insights on how the problem evolved and the abstractions need it. Thanks for this!!

[cupajoesir]

propositions as types, proofs as programs, simplification of proofs as evaluation of programs. very cool stuff.

[mahmedaa]

This is a great talk. And the best part of it is the Q&A at the end. Very informative presentation and even more thoughtful and great questions. I'll certainly come back and watch it again. Thanks Dr. Wadler!

[DumblyDorr]

This is perhaps my favorite talk about the Curry-Howard part of the Curry-Howard-Lambek correspondence. Phil also has talks about the other part (category theory), but there's so much to dive into here - Kleisli and Eilenberg-Moore categories, Lawvere theories etc., but most of all the general idea that things can be fully described by the relational structure they exhibit to the rest of the "universe".

Fortunately, category theory has by now fully arrived in the FP world (~25 years from the discovery of Monads in FP?) - and there are many great talks on the subject.
Dependent Types are still a fringe phenomenon in actual programming (path-dependent types in Scala and Typescript are probably the closest we've gotten in languages that are at least somewhat widely used in the the industry). Linear Logic and linear types have gotten some traction in certain semgents of the programming world, but to my knowledge, nothing concrete has manifested in productive programming languges. (Though please feel to correct me).

[aion]

Last question is the best. Definitely my new favorite talk.

[RobertBerger]

Mind expanding, plus he has a cape too.

[mohammadrezamohammadifar]

The best explanations of proof, type, and history of algorithms! Seems a category? Yes I guess. Thanks a million man.

[robhp]

Amazing lecture! So many important ideas and discoveries shared in less than a hour! Thank you Philip!

[scitwi]

33:55 For a moment I thought he will say "Thank you very much, and I will now take off" :)

[paryoticu]

"[The core of Functional Languages] is not arbitrary. Their core is something that was written down once by a logician, and once by a computer scientist. That is, it was not invented, but discovered. Most of you use programming languages that are invented, and you can tell, can't you. So this is my invitation to you to use programming languages that are discovered."

[valentinussofa]

Amazing talk. Very informative. Thanks for who discovered all this beatiful things in CS.

[Magnetohydrodynamics]

Regarding the name "Computer Science, " Peter Naur (The 'N' in BNF syntax specification) called it "Datalogy" — the study of data.

[EmadGohari]

That was an amazing lecture. very insightful!

[julianfogel]

Wadler leaves out one critical consideration with his superficial criticism of the computer industry for not programming in languages built from lambda calculus. Cost, both in terms of computational complexity and in programmer's time.

He brings up the example of garbage collection to prove his point that industry is too slow (stupid?) at adopting good ideas. The reason it wasn't adopted earlier is because it comes with a rather high cost in computing time and space that older machines couldn't handle. The reason it's adopted now is because the machines are faster and so capable of performing garbage collection in a reasonable amount of time, and since it saves programmers the from the work of coding release of memory by hand in all their work, it's now very cost-effective.

[nmarcel]

A possible solution to the "Independence Day" computer virus plot device: The scientists at Area-51 had 50 years to learn and play with the computer of the crashed aliens spaceship, so they developed a framework to interact with it. So, the code that we see in the movie is a DSL executed against that framework, which in turn translates the intended semantics to the alien computing system.

[someonesomebody]

I am.looking forward to understanding verbal and real.propositions in logic

[raymondrogers]

Prepare to think; it's not "dumbed" down and the "motivation" is only done in passing.

[Dystisis]

"3 things were proven at the same time, that's powerful evidence that mathematics is discovered, not invented" -- We have separate simultaneous/concurrent inventions all the time. It is very common that e.g. two or multiple instrument manufacturers arrive at similar designs or solutions to technical problems. It is no wonder that this occurs. The level of development depends at least in large part on the development of society more broadly. It is the same in mathematics -- it is always linked to technical, social, economic, etc. circumstances.