The Coq mailing list

[Wolfram Kahl <kahl AT cas.mcmaster.ca>]

On Wed, Sep 19, 2012 at 07:04:04PM -0400, Kristopher Micinski wrote:
> On Wed, Sep 19, 2012 at 6:56 PM, Jonas Oberhauser 
> <s9joober AT gmail.com>
>  wrote:
> > Am 17.09.2012 19:47, schrieb Adam Chlipala:
> >
> >>   I think Coq is the secret weapon for addressing this challenge, but I
> >> also think we need some new tool and library support to present Coq in a 
> >> way
> >> that doesn't send first-year university students running and screaming.
>
> [...]
>
> I've been looking and thinking about how you would introduce freshmen
> to discrete math using Coq, and again looking at the Gries and
> Schneider book "A Logical Approach to Discrete Math," I rather like
> it...

In my first-year second-term course, I am using a proof checker I started
to develop for proofs written in LaTeX in the style of that book (LADM):

  http://CalcCheck.McMaster.ca/

Students can use this on their own machines to see whether their proofs are 
good.

One of the advantages I see in the approach of LADM is that at least in
the beginning, the proof format is very rigid, so that it can more easily
be clear to the students what a good proof is. CalcCheck is just intended
to help with the process of learning the details of what a good proof is,
but not to help with finding proofs.


Wolfram