The Coq mailing list

["Pierce Benjamin C." <bcpierce AT cis.upenn.edu>]

>> 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