Climbing the Coq learning wall
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):
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.