The Coq mailing list

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

On 09/25/2012 05:27 AM, bertot wrote:
> Here are a few ideas that can be debated.
>
> - We don't need to restrict to discrete maths.  Reasoning about real 
> numbers is a good playground for learning mathematics. Epsilon-delta 
> proofs, as can be seen in elementary calculus are a good example of 
> where rigor is provided by the proof system.

Handling real numbers is certainly a plus, but I would like to keep 
everything nice and constructive in a first discrete math class.  I 
would probably give in and add excluded middle and functional 
extensionality, but not classical real numbers. :)

> - Concerning automatic grading, I have a few doubts.  What do you want 
> to verify?  The capacity to make a complete proof?  Okay, but what 
> about nearly good proofs?  I fear you cannot measure progress if you 
> only have the "yes/no" answer of whether the students has completed 
> the proof at all.  It is more important to see the student learn to 
> build her understanding of where to use a proof by induction or not, 
> how to load inductions, etc...  This is still too qualitative to be 
> captured by any interactive theorem prover, I fear.  I believe that 
> the main reason why interactive theorem provers have not been adopted 
> by the mathematical community is that they cannot measure "essentially 
> good mathematical proofs".  Still, I have always dreamed that students 
> are happy to verify their own work on their own by seeing that they 
> are able to get the interactive prover's assent.

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.