The 2012 edition of the Oregon Programming Languages Summer School was another huge success, drawing a capacity crowd of 100 eager students anxious to learn the latest ideas from an impressive slate of speakers. This year, as last year, the focus was on languages, logic, and verification, from both a theoretical and a practical perspective. The students have a wide range of backgrounds, some already experts in many of the topics of the school, others with little or no prior experience with logic or semantics. Surprisingly, a large percentage (well more than half, perhaps as many as three quarters) had some experience using Coq, a large uptick from previous years. This seems to represent a generational shift—whereas such topics were even relatively recently seen as the province of a few zealots out in left field, nowadays students seem to accept the basic principles of functional programming, type theory, and verification as a given. It’s a victory for the field, and extremely gratifying for those of us who have been pressing forward with these ideas for decades despite resistance from the great unwashed. But it’s also bittersweet, because in some ways it’s more fun to be among the very few who have created the future long before it comes to pass. But such are the proceeds of success.
One goal of the summer school is to explain the true nature of programming languages research. Most people seem to think that PL research must consist of arguing about semicolons and curly braces, or chasing the whims of some company that’s promoting some language, making marginal contributions in order to be able to say you’re “relevant”. Indeed, in many quarters “relevance” seems to be all there is to the enterprise. But, to paraphrase Kane’s business manager, Mr Bernstein, it’s no trick to be relevant … if all you want to do is be relevant. Indeed, the standard method is to reimport into academics whatever is happening in industry at a given moment, et voila, you are relevant. And deadly boring! To me the goal of research is precisely to be irrelevant to whatever is happening now, with the idea that by the time your ideas become relevant you’ll have moved on to something far more interesting, and far more unimportant to current practices. So my advice to someone embarking on a research career is dare to be irrelevant.
What PL research is really about is nothing short of a general theory of computation that, unlike the narrow interpretation of “theory” that is dominant in the U.S., takes full account of abstraction and composition. Anyone who has ever written code understands the central importance of these concepts, but those who have not seem to regard them as not worthy of consideration—witness the over-emphasis of the Turing Machine as a model of computation, and its emphasis on bit strings as the only form of data. A model that supports neither composition nor abstraction is not much of a model at all, in contrast to the (typed) λ-calculus, which takes both as a starting point. Computational trinitarianism is the proper framework for a full understanding of the theory of computation, and, accordingly, this was a central theme of this year’s summer school, with Frank Pfenning lecturing on proof theory, Steve Awodey on category theory, and me lecturing on type theory. The other lectures built on and extended this foundation to bring students up to the latest research topics in the field, including the use of proof assistants for language meta-theory and compiler verification.
Videos of the lectures, and course notes provided by the speakers, are all available at the OPLSS 12 web site.