The Coq mailing list

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

On 09/17/2012 06:46 PM, Kristopher Micinski wrote:
> One of these problems is pragmatic, we don't have enough good
> libraries equipped with tools (tactics, examples, documentation,
> etc..) to help in teaching (e.g.,) an undergrad class.  This can
> potentially be fixed, but I agree that a real challenge is being able
> to construct a comprehensible and usable theory (and also nontrivial:
> a book / set of examples to go along with it) such that you can use it
> in an instructional environment.
>    

I agree, and this is what I've pointed a few students toward working 
on.  I think it's the primary challenge for using Coq in an introductory 
discrete math class, but I also think it's doable.