Toronto-based reading group that meets weekly to read computer science books and papers.
Currently reading: The Little Typer
Hey Everyone! So it turns out that simplifying logic proofs is equivalent to evaluating computer programs, what!?
In our drifting slide through the theory of types and programming languages, last week we careened into Philip Wadler’s lovely new paper, “Propositions as Types”, which serves as introduction, historical guide, and comic relief to the deep and (at least still for me) magical and mysterious result that logic and program evaluation are deeply entangled with each other. For those with shorter attention spans, he covers a lot of the comedy and history as a quite succesful comedy routine, http://youtu.be/GnpcMCW0RUA, again, what!?
Ricocheting off of our first Wadler paper, this Friday we will start our way through another of Wadler’s papers, “Theorems for Free”, at the usual time and place, 6:30pm at Bento Miso.
I really enjoyed reading this paper, it’s accessible, it has a lot of funny historical anecdotes and he ties them together with both the personalities involved and where they fit conceptually in a greater academic context. The core relation between logic and program evaluation is explored via a clear and pleasantly didactic introduction to the notation for proofs in natural deduction (section 7) and for simply typed lambda calculus (section 8). There is a lot here and the breadth of topics led to a lot of stimulating discussion and to one of the longest sessions to date, although I don’t think any of us noticed the time.
One thought I had while leaving is that often while writing programs you approach things from an aesthetic or design perspective, but this isomorphism tells us that maybe under our aesthetics there is a clear precise mathematical truth. I’m not sure if that last statement is true, but it’s tantalizing to think that you can pin down design concepts into a mathematical equation. I remember being very excited reading all the books I could about chaos theory and fractals. I was at an impressionable age so I believed all of their predications, especially the early super enthusiastic ones; equations to solve nature, everything from weather patterns to the social dynamics affected by your choice of tie, but then when I finally got past the fanciful claims all I got was a fistful of ferns.
Maybe we can keep iterating on this and come up with something, Until next time, Scott?