The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

On Wed, Sep 19, 2012 at 6:56 PM, Jonas Oberhauser 
<s9joober AT gmail.com>
 wrote:
> Am 17.09.2012 19:47, schrieb Adam Chlipala:
>
>>   I think Coq is the secret weapon for addressing this challenge, but I
>> also think we need some new tool and library support to present Coq in a 
>> way
>> that doesn't send first-year university students running and screaming.
>
>
> Although this does not address your issues directly, I took a course
> covering Coq in my second semester and to much benefit, as I feel. I have
> also urged other students to do the same and could convince at least two
> other second semester students to take that course. Although the course was
> slightly different from when I took it, the feedback from the other second
> semester students was positive. (I have also received feedback from other
> students I urged to take the course and the feedback was ... mixed).
>
> For me working with Coq gave me a lot more structure my thoughts and a more
> analytical view on proving and mathematics as a whole.
> I hope that if such classes could be established, other students can profit
> in the same way. While I was a tutor I have seen how some students approach
> proving and I was shocked.
>

May I ask the range of topics covered?  I think the consensus here is that:

  -- Coq provides a great interactive (and more importantly,
*accountable*) style for learning formal mathematics.
  -- Being based on type theoretic concepts, it's natural to teach
things that look like (can be encoded easily in) type theory using it.
  -- Doing so with freshmen / sophomore classes requires careful
planning so as not to force students to battle these topics directly.
  -- A first start to this will be identifying a good base set of
material that can be formalized (definitions written, theorems proved,
tactics provided, book written) for teaching a first / second year
class.

I've been looking and thinking about how you would introduce freshmen
to discrete math using Coq, and again looking at the Gries and
Schneider book "A Logical Approach to Discrete Math," I rather like
it...

kris