4 ms·

Opinion of a programmer learning Coq: I think the Coq program is THE proof, everything else is aesthetic. I quite do not like the idea proposed in the paper to

Opinion of a programmer learning Coq: I think the Coq program is THE proof, everything else is aesthetic. I quite do not like the idea proposed in the paper to comment every Coq line. There is risk to give an illusion of understanding. Whereas true understanding occurs when following side by side the Coq code and the evolution of the goals, and agreeing with the prover. To me, it is like following a proof on the blackboard. You may think you have understood, and stumble when doing it on paper. Doing the proof in Coq and forcing me to understand each step gives me the impression to do it on paper ... well sometimes I write bits on paper when the prover still goes too fast.

zozbot234 7y ago
> Whereas true understanding occurs when following side by side the Coq code and the evolution of the goals This is the only way to understand a proof script, because proof scripts in and of themselves are totally opaque. It's like running a function with no source information step-by-step in a debugger. Declarative proofs are high-level (and can in fact be made arbitrarily-high-level by omitting proof steps and turning them into well-structured "sketches") and give you the equivalent information within the source code.
tom_mellior 7y ago
> 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.

zozbot234 7y ago

> Whereas true understanding occurs when following side by side the Coq code and the evolution of the goals This is the only way to understand a proof script, because proof scripts in and of themselves are totally opaque. It's like running a function with no source information step-by-step in a debugger. Declarative proofs are high-level (and can in fact be made arbitrarily-high-level by omitting proof steps and turning them into well-structured "sketches") and give you the equivalent information within the source code.

tom_mellior 7y ago

> 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.