Lambda the Ultimate

I was just a gadfly, so LtU folks who actually presented etc. at the unconference can talk more in-depth, but it seemed to me that Scala is getting serious momentum. More power to it, we could stand to have a "better" Java.

[Edit: I am promoting this to the front page. Click to read more details, as they are posted to the discussion group. -- Ehud]

In Fall 2007, I taught an introductory course on logic and the theory of programming languages entirely in Coq. The experience was quite demanding — for the students and especially for me!— but the overall payoff in terms of student engagement and performance on exams far exceeded my hopes. I am now convinced that this is the right way to teach programming language foundations and am working on course materials that will allow the approach to be replicated elsewhere.

Just this weekend I talked with someone about E-Learning, and he mentioned "immediate nonjudgmental feedback" as one of the main advantages of using computers in the classroom. In the context of teaching logic and the art of constructing proofs this boils down to using proof-assistants as "personal TAs". This is what Pierce tried to do (Paul will be pleased: Coq was the proof assistant Pierce chose), and this note describes his experiences and conclusions.

The teaching materials are available online, if you prefer to look at them and form your own opinion before reading Pierce's conclusions...