Wadler's act in StrangeLoop ●

October 18, 2015

technology, fun-prog

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.1

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 2

  • 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

  1. I’ve attempted the paper more than once before and still for a mere undergraduate with limited knowledge of formal logic it’s really deep and tough to get all the points. This explanation of him encourages me to go back to it again and may be this time I will be able to extract more things from it ↩︎

  2. while working nowadays on technologies for Semantic Web, one aspect of Informatics that relates to structuring data for the web, I am drawn more than often to model systems via first-order logic constructs and clearly I could realise the power of structuring information that way so that they can be leveraged further for more amazing discoveries ↩︎