The Coq mailing list

[Jean Goubault-Larrecq <goubault AT lsv.ens-cachan.fr>]

Benjamin Pierce wrote:
> My questions for the group:
>    - Is this insane?
>    - Have other insane people tried it previously --
>      either in undergraduate / masters level CS courses, or simply  for 
> teaching basic logic?
>    - With what results?
>    - Any lecture materials / advice to share?

        Dear Ben,

        I've tried something similar eight years
ago at ENSTA, an engineering school here in Paris
(ENSTA="national superior school of advanced techniques").
This was in a series of 6 lectures, each 3 1/4 hours long,
on formal methods, typically specification languages.
This was intended for 3rd (last) year students, i.e.
roughly masters level.  We only dealt with Coq in the last
two lectures, organized as exercise sessions on PCs.
        See http://www.lsv.ens-cachan.fr/~goubault/cours.html#svl
(in French), where, as you see, I've put a small
cryptographic protocol example, a logic puzzle,
Peterson's mutual exclusion example, and the correctness
of a heapsort procedure.
        All in all, I guess that almost all students grasped
the idea without any serious problem.  One really could not
grasp even the beginning of it.
        On the negative side, I never managed to convey
to (most of) them the importance of verifying software or of proving
the correctness of software.  They definitely felt that
specification was not "real life", and that Coq was some
kind of theoretician's delirious dream.  They still did
the exercices, with some success, though.
        Best,

        -- Jean Goubault-Larrecq
        (LSV/ENS Cachan & CNRS UMR 8643 & INRIA projet SECSI).