3 ms·

I think here is room for some literate programming here. Why not have once source document for both formal proofs and semi-formal expositions. Then one can extr

by cjfd 7y ago

I think here is room for some literate programming here. Why not have once source document for both formal proofs and semi-formal expositions. Then one can extract from that the coq proof and thus have a proof that everything is sound and also extract a LaTeX document that is nicely readable. In particular one would probably not extract proof bodies because coq proofs are not that readable but replace them by semi-formal proofs that are also included in the same source document.

zozbot234 7y ago
Coq used to support a "declarative proof mode" that's a lot more readable and maintainable than the usual proof scripts. Older versions of Coq could even output a pretty-printed version of any proof term, where the structure of the corresponding proof was explained in English text. Very old versions of Agda had an even more developed support for "literate" proofs, where any item in the proof language could have a natural-language form, that could also be endowed with features in natural language grammar (singular/plural forms, grammatical class such as noun/adjective/verb/adverb, symbolic vs. written out form) and thus allow for complex phrases to be pretty-printed automatically. All of these features were left to bitrot, unfortunately. I don't think the version of Agda I mentioned can even be downloaded anymore. (Newer versions of Coq have some support for 'structured' proofs that is supposed to improve maintainability if proactively used, but it's a far cry from what those features could allow 'out of the box', with no need for special care or discipline from the user.)
- tom_mellior 7y ago
  > Coq used to support a "declarative proof mode" that's a lot more readable and maintainable than the usual proof scripts. I liked playing around with that, but it was quite restricted in what it really do. And it lacked the automation that Isabelle/HOL has. In Isabelle you can really focus on the general structure of the proof and have it fill in the intermediate steps by automated theorem proving. In Coq's mathematical proof language I remember having to write a lot more of hand-holding code. Isabelle's Isar proof language is not quite as readable as textbook proofs, but it does make proofs somewhat "informally" readable. There are some nice examples in https://isabelle.in.tum.de/library/HOL/HOL-Isar_Examples/document.pdf https://isabelle.in.tum.de/library/HOL/HOL-Isar_Examples/doc... (though the very first one is not the nicest, I think). Edit: Forgot to mention, the above document is kind of what the OP asked for, you can generate this kind of LaTeX document from a fully formally checked Isabelle/HOL development.
  - jerome-jh 7y ago
    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.
- mietek 7y ago
  The current release of Agda supports literate markdown. https://jesper.sikanda.be/posts/literate-agda.html https://jesper.sikanda.be/posts/literate-agda.html

by cjfd 7y ago

zozbot234 7y ago

Coq used to support a "declarative proof mode" that's a lot more readable and maintainable than the usual proof scripts. Older versions of Coq could even output a pretty-printed version of any proof term, where the structure of the corresponding proof was explained in English text. Very old versions of Agda had an even more developed support for "literate" proofs, where any item in the proof language could have a natural-language form, that could also be endowed with features in natural language grammar (singular/plural forms, grammatical class such as noun/adjective/verb/adverb, symbolic vs. written out form) and thus allow for complex phrases to be pretty-printed automatically. All of these features were left to bitrot, unfortunately. I don't think the version of Agda I mentioned can even be downloaded anymore. (Newer versions of Coq have some support for 'structured' proofs that is supposed to improve maintainability if proactively used, but it's a far cry from what those features could allow 'out of the box', with no need for special care or discipline from the user.)

tom_mellior 7y ago
> Coq used to support a "declarative proof mode" that's a lot more readable and maintainable than the usual proof scripts. I liked playing around with that, but it was quite restricted in what it really do. And it lacked the automation that Isabelle/HOL has. In Isabelle you can really focus on the general structure of the proof and have it fill in the intermediate steps by automated theorem proving. In Coq's mathematical proof language I remember having to write a lot more of hand-holding code. Isabelle's Isar proof language is not quite as readable as textbook proofs, but it does make proofs somewhat "informally" readable. There are some nice examples in https://isabelle.in.tum.de/library/HOL/HOL-Isar_Examples/document.pdf https://isabelle.in.tum.de/library/HOL/HOL-Isar_Examples/doc... (though the very first one is not the nicest, I think). Edit: Forgot to mention, the above document is kind of what the OP asked for, you can generate this kind of LaTeX document from a fully formally checked Isabelle/HOL development.
- jerome-jh 7y ago
  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.
mietek 7y ago
The current release of Agda supports literate markdown. https://jesper.sikanda.be/posts/literate-agda.html https://jesper.sikanda.be/posts/literate-agda.html