The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

On Mon, Sep 17, 2012 at 6:53 PM, Adam Chlipala 
<adamc AT csail.mit.edu>
 wrote:
> 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.

If you consider or solicit other people for this task, I'm sure others
would be similarly interested, and it seems the SF book also benefited
(to some extent) by external contributions too.

kris