These guidelines have been used for POPL this year, which is a very good thing. There is however one part of the guidelines that I would like to react:
Check whether the code contains undocumented assumptions or unfinished
proofs, such as the use of “Axiom” or “Admitted” in Coq, “postulate” or
“{!!}” in Agda.
I strongly disadvocate the look for Axiom or Admitted in Coq: my own proofs use (documented) axioms, but they would be invisible to such a keyword search. The reason is that there are many ways to hide axioms in Coq: TLC’s skip tactic makes use of an axiom without using these keywords, there is an axiom of False in Coq’s standard library, etc.
Instead, I strongly encourage Coq reviewers to use the Print Assumptions command (see https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.print-assumptions ) on the main theorems: it provides a much more detailed view on what axioms have been used for this particular
theorem and its dependencies, and is much more powerful than any grep command.
I have no idea whether other theorem provers have a similar command, though.
These guidelines have been used for POPL this year, which is a very good thing. There is however one part of the guidelines that I would like to react:
I strongly disadvocate the look for
AxiomorAdmittedin Coq: my own proofs use (documented) axioms, but they would be invisible to such a keyword search. The reason is that there are many ways to hide axioms in Coq: TLC’sskiptactic makes use of an axiom without using these keywords, there is an axiom of False in Coq’s standard library, etc.Instead, I strongly encourage Coq reviewers to use the
Print Assumptionscommand (see https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmd.print-assumptions ) on the main theorems: it provides a much more detailed view on what axioms have been used for this particulartheorem and its dependencies, and is much more powerful than any grep command.
I have no idea whether other theorem provers have a similar command, though.