The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

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.

Kind regards,
jonas
PS: I'm currently working on my bachelor thesis (using Coq).