The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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.