How to Prove a Statement That Is Not Provable

Tech Talks are in-depth technical discussions.

Today I talk to Professor Philip Wadler, a very accomplished programming language researcher.  Phil walks us through a principle that has guided his career.  That principle is that typed lambda calculus is not invented but a discovery of a deep truth. It is something connected to the mathematical underpinning of the universe itself.

It follows from this that functional programming languages are therefore more correct or more deeply justified and fundamental than other languages.  I am probably stating things in a stronger fashion than Phil is comfortable with, but I like fp, so I can be a little hyperbolic.

While explaining this principle, that has guided his career, Phil takes us through the history of computer science.  We start with Turing and Alonzo Church.  Eventually we get to what the movie Independence Day got wrong and what language a theoretical creator deity would program in.

• talk
• paper

Web page for this episode

CoRecursive On Twitter

CoRecursive On Itunes