Home

Lambda, the Ultimate TA

Benjamin C. Pierce. Using a Proof Assistant to Teach Programming Language Foundations, or, Lambda, the Ultimate TA. April 2008. White paper.

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...

By Ehud Lamm at 2008-05-12 20:29 | Teaching & Learning | other blogs | 17785 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

this eases my stress

I found Coq to be very powerful but also difficult. Now I don't feel so bad. I would like to see e-learning workbooks for Shriram Krishnamurthi's PLAI and also HtDP.

By Geoff Knauth at Wed, 2008-05-14 22:52 | login or register to post comments

Bash 'n' Me

I've been printing the lectures out and reading them on the train rides home (where I can excuse myself for not doing "real work"), but have been frustrated by the lack of Coq interpreter feedback. Other Coq tutorials print the interpreter's feedback after commands, which makes it much easier to read.

I had a hard time getting this output properly formatting from Coq. ("coqtop -lv" destroys comments; just tee-ing the output to a file didn't include the input; and pasting the text into the terminal and then saving that from the terminal would jumble input and output text.)

The best I could come up with was to run

rlwrap -l lec07withoutput.txt coqtop

and then paste in lec07.v (for example) into the terminal.

Are there cleaner ways of doing this with coq?

By aed at Fri, 2008-05-16 23:10 | login or register to post comments

Maybe...

...Proof General?

By Paul Snively at Fri, 2008-05-16 23:36 | login or register to post comments

Well...

...from this screenshot, I get the impression that proof general resembles CoqIDE, where code and results (especially the current goals, and how tactics have changed the shapes of the goals) are shown in separate areas.

The format I hope to imitate is that of the standard Coq tutorial, where input and output are shown together, in order. Coq proof-tactical code is more readable (to me) in this format.

By aed at Sat, 2008-05-17 00:30 | login or register to post comments

Thank you

... for making this lecture available on the net! To me, this seems to be one of the best resources for learning the fundamentals. I am still on the fourth lecture (going through everything carefully takes a lot of time) and am waiting for TAPL to arrive, but already, I feel like I'm learning a great deal about how to use Coq as well.

By ttsuchi at Tue, 2008-05-27 19:20 | login or register to post comments

Great and simple way to learn Coq

For me, these lectures have proved to be a great and simple way to learn Coq. Great, because they're goal-directed. Simple, because they're hands-on.

By namin at Sun, 2008-08-17 12:02 | login or register to post comments

New presentation and new book

A couple new developments in this story.

Pierce recently gave a talk at ICFP about this that I recommend.

Also, there seems to be a new online book version of the course materials.

I have recently gone through this material doing all the exercises as a more personally-motivating tutorial for Coq. (My previous attempts at mastering Coq have tended to run aground on examples that lacked motivation for me, in both senses of the word.)

I think this material can be recommended for two groups: those who already have a grounding and interest in PLT and want to learn Coq, and those who are used to programming but find following proofs, say in TAPL, difficult.

Though I'm not a member of the latter group, I was surprised how effectively this material allowed me to think about proofs purely with the "programmer part of my brain", without having to resort too often (except at the highest level) to the "proof-reader part".

For those in the former group, I can attest that, having finished this material, I burned through the Coq'Art book getting a LOT more out of it than my first pass through, and I'm left with the sense (or at least the very strong illusion ;-)) that I could actually use Coq "for real" now.

By Marc Hamann at Thu, 2009-11-05 17:26 | login or register to post comments