I agree you that the second proof is complete. I've been experimenting with Coq[1] recently, which I really hope could be the best of both, where everything is

I agree you that the second proof is complete. I've been experimenting with Coq[1] recently, which I really hope could be the best of both, where everything is formalized and complete (or else the compiles yells at you), but it's easy to build new abstractions and reference prior proofs, in a way that lets the reader just to the definition with a keystroke. It's harder to use than I want it to be though. Still, I would recommend checking it out if you like explicit formal proofs. It's really good at that. [1]: http://coq.inria.fr/ http://coq.inria.fr/ Also, I know how hard it can to get started. It really does help to have someone to ask dumb questions to, so feel free to email me (email in profile), or ask on SO.