I also find this way cool. You will probably enjoy Wadler's Propositions as Types if you want to understand the proof/program thing in more detail. I am generally interested in program analysis and theorem proving and that sort of thing. I picked it up to maybe use it with my research, since being able to generate proofs and extract executable code is pretty handy, but we'll see if I can become competent in it fast enough to be able to actually apply it. Also I like roosters I did write another thing about using Coq that shows some of the proof state as you go. The interactive part really makes writing proofs possible; I don't know if I could just look at something and write all the ltac for it without any help. This is a bit more along the lines of what I'm doing for research, but still a long ways from what counts as cutting-edge nowadays :)