The Coq mailing list

[immanuel litzroth <ilitzroth AT gmail.com>]

Hi Adam,
I for one would be very interested. I'm currently doing a MITx course
in electronics
on the advice of one of my colleagues and I'm very much enjoying it. Moreover 
at
my workplace (I do C++ programming) there are several people who have 
expressed
frustration in learning and using coq -- we do have some stuff the we
would like to "prove
correct" -- so I guess I'd be bringing between 3 and 6 people along!
Kind Regards,
Immanuel Litzroth

On Mon, Sep 17, 2012 at 7: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.
>