free variable

Benjamin Pierce developed a graduate PL theory course based on TAPL. This isn’t that surprising, since TAPL is an excellent text and I suspect Pierce knows it rather well. The exciting part is that he taught the course with Coq, which is a pretty cool development. His report on the experience, “Using a Proof Assistant to Teach Programming Language Foundations, or Lambda, the Ultimate TA,” looks worth reading.

I like the general idea: interactive development in a proof assistant does for novice proof-writers what interactive development in a conventional programming language does for novice programmers. I also recall being a frustrated undergrad in my first class with a proof component precisely because it wasn’t always clear — before one handed in the assignment, that is — what constituted a good proof and what didn’t. However, Pierce rightly points out that teaching students to write formal, machine-checked proofs doesn’t necessarily help them to write informal proofs. (Also, Coq error messages aren’t always helpful feedback — but they’re at least as good as the worst feedback students get from a human on paper proofs.) I’m delighted to see this development, though — I’ve been thinking about the possible didactic benefits of proof assistants since I took non-classical logic early in grad school, and it will be interesting to see how Pierce’s work plays out in the larger CS pedagogy scene.