As I mark exams for this academic year, it is time to think about how it went this year and what I can do to improve the module Programming Language Design and Semantics (CS332)next year.
I am very fond of this module, as my colleague David and I designed it soon after I arrived here and a bit before David, alas, left. The idea was that he would teach the formal semantics aspects, while I would be responsible for helping students articulate their thoughts on the design of languages. I based this idea on my roots at UC Davis, where the undergraduate PL module covers several language paradigms at a very practical level, and a great book I came across there, Programming Languages, a Grand Tour, ed Horowitz, a wonderful collection of classic opinion pieces written by language designers and users–sadly out of print, I couldn’t even find a proper link to this book, though I guess now one can build the same collection of papers as a webpage – and maybe someone has already done this.
Meanwhile, though my colleague David left, my new colleague Ranko has taken on the mantle and has been doing a great job teaching the tradition, formal semantics aspects, with coverage of the operational semantics of a toy While language and the proof of correctness of its abstract interpreter. During a teaching shuffle I lost this module, and while I wasn’t watching the design aspect of the module was taken out of the syllabus, unfortunately.
Operational semantics is (in my opinion) required background for every computer scientist. However I feel there is a real and increasing need to give a solid background on other aspects of semantics, namely types and formal type systems–after all objects, modules and polymorphism are what distinguish modern languages, and where many advances are happening on the landscape of programming. So in the last couple years, since I got myself back as an organiser for this module, I have incorporated several weeks covering type systems, and in particular the treatment given in Cardelli’s classical handbook chapter Type Systems and the elegant notes used by Andy Pitts at Cambridge.
I am thrilled to be teaching this material, but I feel the students are finding it hard going. I think the main issue is that there don’t seem to be textbooks targeted at the undergraduate level that cover this material in a very accessible level. I have the classical textbooks by Gunter, Pierce, and Mitchell, and while these are extremely solid and beautifully written (and, I just realize, all published by MIT Press), are at a level that is not appropriate for students who do not have the required background. I end up consulting these books and basing my lectures on just a few pages from each…
The first part of the module, where I cover Lambda Calculus and introduce simple types, is served by many notes available online, such as Barendregt’s notes, but there is still a lack of exercises of slowly increasing complexity to train the students in building type inference trees and understanding issues in type soundness in relation to actual programming languages. And then to transition from this language to the ML type inference, and from there to more advanced type systems is quite a challenge.
The idea crosses my mind that I should sit down for a month and really try to develop a coherent set of notes which covers this material in small baby steps. But before that, a question to the ether: does anyone know of any good resources and specifically textbooks that cover this kind of material aimed at undergraduates? Any pointers much appreciated.