The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

Dear Adam,

are you aware of the ForMath project,
http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ForMath ? It
seems relevant to what you are talking about. See for example the math
classes library at http://math-classes.org. In general, formalization
of mathematics is a non-trivial issue.

It would be interesting to see an experiment in teaching math through
a proof assistant. I think it is quite hard to do so well. It may be
the case that a Coq library for research-level math, or
"system-building" math is not appropriate for teaching. Who knows,
nobody has ever tried!

With kind regards,

Andrej

On Mon, Sep 17, 2012 at 1:47 PM, Adam Chlipala 
<adamc AT csail.mit.edu>
 wrote:
> I'm interested in applying Coq in teaching university students mathematical
> subjects, including the theory underlying computing.  This message is meant
> to get a sense of who out there is interested in collaborating to build the
> necessary tool support.
>
> A bit of my personal context: I teach at MIT, which has a newish initiative
> MITx, for running online classes, with opportunities to apply the same
> technology to augment traditional in-person education.  Automatic grading is
> a central part of the approach, and one of the biggest scaling challenges
> has been grading assignments where students write mathematical proofs.  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'm
> doing some initial work in this direction with students, but I think this is
> an idea that could really benefit from a broad community effort.
>
> So, I have two primary questions to ask:
>
> 1. Would any Coq experts be interested in spending some time at MIT as
> postdocs or research scientists, building the support for applying Coq in
> early university classes relevant to computer science?  Please let me know
> if so!
>
> 2. Could we as a community create an open platform for contributing Coq
> libraries relevant to different modules of different courses?  A nice user
> interface would be crucial, and it wouldn't be any good for each university
> to roll its own.  I would like to see a web-based interface, with bonus
> points (from my perspective) if it uses my language Ur/Web
> <http://www.impredicative.com/ur/>. :)  I also feel that we need
> course-specific tactic libraries, to allow proofs to be written at the right
> levels of abstraction, without overwhelming students.
>