The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

On Mon, Sep 17, 2012 at 6:36 PM, Pierce Benjamin C.
<bcpierce AT cis.upenn.edu>
 wrote:
>>> You are aware that the university of Pennsylvania teaches a course using
>>> the software foundations textbook which slightly satisfies this idea? It's
>>> the closest thing I can think of off the top of my head. I believe Pierce
>>> has a talk on it, lambda the ultimate ta.
>>
>> Software Foundations is a great textbook, but it focuses on aspects of
>> mathematics and programming languages theory which traditionally theorem
>> provers like Coq have been quite strong at.  I believe Adam is interested
>> in targeted mathematics that goes beyond the simple structural induction
>> we know and love.
>
> Yes, PL foundations is the easy case for teaching using Coq.
>
> I think one next (big) step should be undergrad discrete math -- help is 
> badly needed there!
>
>     - Benjamin

I agree with everything said, and Adam also echoed this to me.. But my
question is, if we take a theory that might not be so amenable to
using Coq (i.e., step outside of the bounds of teaching the core of
Coq, largely the ideas underpinning PL), what kinds of problems will
we run into?

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.  Where your typical Coq hacker may
stand on their head and use some more complex environment, this notion
will likely evade undergrads, since (not having experience with Coq)
they will be largely focused on comprehending the knowledge in the
theory, rather than the tool.

So it seems to me that the problem right now is that undergrads
approaching Coq would mostly be battling the tool itself, with the
theory as an ancillary point of confusion.  In reality, we would
prefer it the other way around.

(I can most certainly attest to having seen many people in TA office
hours, or classmates say "oh well, I have to go off and type stuff
into coq until it tells me the proof is completed," I would fear a
course in discrete math would devolve into this without a lot of care
taken to avoid it.)

If anyone plans to start such a development, I would gladly contribute
to such a book..

Kris