> Whereas true understanding occurs when following side by side the Coq code and the evolution of the goals In addition to the sibling comment, this also break

> Whereas true understanding occurs when following side by side the Coq code and the evolution of the goals In addition to the sibling comment, this also breaks down in the presence of using elaborate Ltac tactics to automate large parts of proofs. There you'll just have a big macro step that eliminates the goal, or transforms it arbitrarily, or fails, in some way you don't necessarily understand. But this kind of automation is necessary for large projects on the scale of CompCert, otherwise you'd die of boredom trying to type out all the cases yourself. Nobody should comment every line of a proof, but they should document the general ideas and structure, and other proof languages than Coq's tactics language do this better. I really urge you to take a look at some of the proofs in the PDF I linked above. You won't understand everything, and I'm not trying to convert you to Isabelle, but you will see a different way of structuring things.