> I would like to work more with actual mathematical proofs but I'm finding that tough to get into myself. A professor at my CS dept. started using the Coq pro

> I would like to work more with actual mathematical proofs but I'm finding that tough to get into myself. A professor at my CS dept. started using the Coq proof assistant[0] to teach some (functional) programming concepts and techniques. It has had a side effect of making the students more in to proofs. Personally I think it's great - it shows that proving things is just programming. I think the Software Foundations book[1] (or tuturial?) is a good place to start. There is also another good tutorial, but I can't remember its name. It's more about "getting work done" so I don't think it's as good as a starter. [0]: http://coq.inria.fr/ http://coq.inria.fr/ [1]: http://www.cis.upenn.edu/~bcpierce/sf/ http://www.cis.upenn.edu/~bcpierce/sf/