Wadler's act in StrangeLoop ●
Philip Wadler explained his seminal paper Proposition as Types [PDF] on stage in StrangeLoop this year with an onceinalifetime act
The whole presentation is mindblowing. 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 pointofviews 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 2530 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

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 ↩︎

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 firstorder 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 ↩︎