The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi all,

I completely agree with Adam: coqchk could be improved as a better
tool for semi-automatic code review. It seems to me that most of what
remains to be done in that aim has to do with defining the workflow,
conventions, etc. but shouldn't be technically too hard.

Also, I agree with what has been said that an important step towards
making vo files the piece that you share around to get reviewed would
be to make these vo files independent of the platform and the OCaml
version (making the format stable across Coq versions would be a great
objective too, but probably not as urgent).

Finally, Emilio, I don't understand what the issue would be with
providing a `-safe` mode that doesn't allow writing to files? Why do
you say a complete redesign and rewrite would be necessary? I seem to
have always heard people be optimistic on this matter (with projects
such as MetaCoq in particular). Your claim seems a bit at odds with
this.

Théo


Le dim. 2 févr. 2020 à 15:52, Adam Chlipala 
<adamc AT csail.mit.edu>
 a écrit :
>
> On 2/1/20 11:30 PM, Timothy Carstens wrote:
> > Consider the following workflow:[...]
> > 5. User runs coqc foo.v
> >
> > [...]
> >
> > If so, then (5) is inherently an unsafe thing to do, and in that case
> > I don't see how Coq could be used to certify untrusted code. You'd
> > need to first do a code review of the ltac and everything else to
> > convince yourself that it was safe to compile.
>
> I think this might be a case of many people on this mailing list taking
> workflow details for granted and not realizing they should be spelled
> out.  No, the clear community recommendation would be to check .vo
> files, not .v files.  However, that mode requires additional code-review
> tools that pretty-print crucial parts of .vo files in sufficiently
> readable ways (definitely not involving Ltac, plugins, etc., and in fact
> with no need to display proof terms, just "final" theorem statements and
> their dependencies).
>
> jonikelee AT gmail.com
>  wrote:
>
> > I once used an
> > antequated proof system (pvs) that had a tactic language but also had
> > the ability to "macro-expand" the tactics into atomic proof steps and
> > record the resulting fully expanded proofs in a file. Having that
> > eliminates the need to run the tactic language later to verify the
> > proof, and thus the possibility that someone can exploit the tactic
> > language.
> That sure sounds like .vo files and, in general, the trust philosophy at
> the heart of the Coq project since the beginning.
>