I was mostly joking, but I'm halfway done with the 1st of these books. It's definitely laborious, but interesting. It seems like things are faraway from production and changing pretty fast in that space. Some others: Agda, Idris, ATS (this seems scary). The most impressive Coq project I've seen is this C compiler: http://compcert.inria.fr .

Btw, juggling with proofs is very video game like though, I played with them too late into the night. That constant feedback! The triumph of writing Qed.