The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

On Wed, Sep 26, 2012 at 5:13 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

Well, to scale to large online classes, it seems hard to give detailed proof feedback to everyone, so I think "yes/no" checking would be at the center of a grading system.  At the same time, it is important for students to learn to write traditional prose proofs, so it might be nice to use crowdsourcing to get them giving each other feedback on proofs.

If you only need more detail on the "no" part: One possibility might be to provide a series of tactics (perhaps in a black box on a webserver or something) that performed increasingly sophisticated methods of solving the goal, and the incremental goals of a student were to move from needing the most powerful tactic to finish the proof for them to needing less powerful tactics.  (It might also be used as a check for "am I going in the right direction?".)

-Jason