The Coq mailing list

[Benjamin Werner <benjamin.werner AT inria.fr>]

    Hi Benjamin, André, Aaron and all,

I am quite convinced that if it is used well, Coq (or another similar  
system) is a valuable teaching
tool and not only a teaching topic.

I have teached Coq to undergrads several years. The two last years, I  
had a few more
time slots and I merged the course "about Coq" with a basic course  
about lambda-calculus,
core ML, typing and operational semantics.

So during the one or two first sessions, I would do basic Coq on one  
hand and programming
language theory only on paper, and then have the two topics merged,  
that is using the Coq
sessions to formalize and implement the concepts discovered in the  
PLT course.

It worked quite well actually, and I think the two components of the  
course benefitted
from each other. The fact that the students know little or no logic  
is not a big problem.

It may be a good idea to teach them some natural deduction once they  
are a little familliar
with the system though.

Some more remarks:

- You can have them write reasonable programs inside Coq. Probably up  
to a small toy
"compiler". Of course, at some point, the lack of side effects,  
libraries and I/O facilities
becomes an issue.

- students knowing ML have little difficulties switching to Coq  
syntax for writing programs.
Students not knowing ML can learn basic functional programming  
directly in Coq.

- I would be careful to have enough teaching assistants knowing Coq  
to help the students,
especially in the begining. It is very eay to stay stucked for a long  
time over a simple problem
when you start learning Coq.


I do not have much written material (let alone in english) right now.  
In any case, I would
be very interested to know how your project will go. I am starting to  
think about proposing
a new course including formal proofs too.

It seems indeed a good idea to have some pages listing such courses  
and pointers to
teaching material !



Best wishes,


Benjamin