The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

Andrej,

You are aware that the university of Pennsylvania teaches a course using the software foundations textbook which slightly satisfies this idea? It's the closest thing I can think of off the top of my head. I believe Pierce has a talk on it, lambda the ultimate ta.

On phone,

Kris

On Sep 17, 2012 5:32 PM, "Andrej Bauer" <andrej.bauer AT andrej.com> wrote:
>
> 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.
> >