For those interested in learning about Coq (and computer science in general), I'd highly recommend http://www.cis.upenn.edu/~bcpierce/sf/current/index.html http

For those interested in learning about Coq (and computer science in general), I'd highly recommend http://www.cis.upenn.edu/~bcpierce/sf/current/index.html http://www.cis.upenn.edu/~bcpierce/sf/current/index.html. Aside from being incredibly enlightening, it's also quite fun. Set it up in emacs with Proof General and you get instant validation that you're correctly doing all the exercises as you go; it's like playing a game that teaches you type theory, proof automation, typed lambda calculus, Hoare logic and more.