CS Cabal

Toronto-based reading group that meets weekly to read computer science books and papers.

Currently reading: The Little Typer

GuildMeetup listings

Mastodon Social Hub

Mailing list Communication nexus

Code of Conduct Must read

PFPL In Memoriam

March 28, 2017

By Inaimathi

This entry has been shamelessly cross-posted from langnostic.

For the past year or so, the Toronto Comp Sci Cabal has been reading a book called Practical Foundations of Programming Languages(PFPL). And the sheer idea density in this thing was giving me enough fodder to chew over and blog about for something like a month after each reading. The trouble is, we met to discuss and read the next section about once a week, so chewing and blogging time has been getting very seriously truncated on a consistent basis. The end result of this will eventually be a series of posts, each focusing on trying to understand a single topic we covered, but I won’t embark on that journey today.

This past Friday, we held the concluding meeting of the reading of that book. It was pretty awesome. We got the entire group back together, and were joined by Bob Harper by video. Even though we’d met him before, it was nice to talk to him once we’d finished reading his work.

The conversation ranged from type theory, to language design, to the current state of programming as a discipline. The definite highlight for me was finally getting to thank him for explaining some of the things that get vaguely and inconclusively discussed in the comment sections of his blog. The big ones are

Those are highlights, but they’re not even remotely the only ideas worth exploring in the book. In Harper’s own mind, some1 of the highlights of the tome are

As that light sprinkling of topics should show you, this book is a comprehensive treatment of the art and science of programming language theory and design, from a perspective that isn’t exactly mainstream in the industry at the moment. Despite all the bitching and silence, I thoroughly recommend reading it. Especially if you think you couldn’t handle it at the moment. Because it will start you from the very basics of proofs, and take you to the height of building solid systems. Because it will challenge many notions that may have become intuitive, but are nevertheless wrong once you look at them closely. Because it will very probably force your brain through the wringer, and enlighten you as few other tomes can.

For our next book, Bob suggests we pick up Reynolds’ Theories of Programming Languages, which we very well may do. However, for the moment we’re gearing up to start on some interesting papers, right after a short and well-earned rest.

  1. He also mentioned that he half considered re-writing the whole thing on the basis of Concurrency and Dynamic Classification. Which are apparently the two features you need in order to implement the rest of everything laid out in the book. I haven’t tried to do this, but it does seem plausible though difficult.