# Wadler’s act in StrangeLoop

Philip Wadler explained his seminal paper Proposition as Types [PDF] on stage in StrangeLoop this year with an once-in-a-lifetime act

The whole presentation is mind-blowing. The way he peeled the layers to show the deep relationship between formal logic and modern computation through historical facts & proofs is a treat to watch.

I saw it more than once, mostly for the fun of it, & here are some of his statements (emphasis mine) that are still ringing in my ears. The notes are in reverse chronological order of the timeline of the presentation as I think some interesting point-of-views came out after the thing happened at around 33:24

- 2 things that are wrong with computer science is
*“computer” & “science”*coz its not just about computers and you don’t put science in it if it’s real science - impact of computer science on knowledge in general
- structuring of information is very important as it will not only help understanding how computers work or will work but also how universe is designed
- how ideas are structure would determine that many new ideas can be discovered
- this is called informatics
*fundamental good idea takes 25–30 years for mass adoption*- it takes a long time for good ideas to come out, so it needs a long perspective if you want to have good ideas, ideas that are discovered not invented
- logicians will always get there first than computer scientists to discover new ideas as they tend to be at there for a longer time
- lambda calculus is omniversal
*real programming languages are discovered not invented*- logicians and computer scientists come up with similar ideas pretty much at the same time i.e.
*every good idea will be discovered twice* *central idea that relate logic to computability (curry/howard correspondence)*- proposition as types
- proofs as programs
- simplification of proofs as evaluation of programs
- Godel was 28, Turing was 23 when they undermine the work of Hilner( then 68) and Church( then 33) & Godel( then 30) respectively. So
*young people should always call out when people older are wrong*. - it all started with “Entscheidungsproblem” by Hilbert when he wanted Mathematicians to come up with an algorithm that can determine given a statement in formal logic whether that statement is true or false in other words he depended on the notion of complete logic which says that “
*every true statement is provable and every provable statement is true*” !!