Climbing the Coq learning wall

So I am currently trying to learn Coq, this is a monstrous and Herculean task. It is one of those things where the learning curve is so steep as to deserve a climbing grade (I reckon about v6 for the intersection of the bouldering and PLT communities).

I have the Coq art book winging its way to me, but due to my remote location at the end of the earth (from the perspective of shipping companies, to everyone else I am in the capital of a developed country a days flight from Europe), it hasn't arrive nearly a month after ordering.

But, I Benjamin Pierce teaches a course on Coq and has made the lecture notes (which are all Coq scripts) available online (link is to 07's course schedule which has the whole course, as opposed to the current one):

http://www.seas.upenn.edu/~cis500/cis500-s09/index.html

This is an excellent tutorial for learning Coq from a PLT perspective and I highly recommend it - more so than any of the other Coq resources I've found online.

So, although tough, learning Coq is actually fun, and I hope will be useful. At the moment doing full proofs for a full calculus seems too daunting, but I can see that it is not as bad as some people make out, and hopefully once I have the hang of things will not be too hard. Also seems like a very interesting place to do research - there are so many things crying out to be studied.