The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

On Sun, 2 Feb 2020 09:51:46 -0500
Adam Chlipala 
<adamc AT csail.mit.edu>
 wrote:

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

If the tools you requested above existed, I might be able to see that
this is the case!  So, that request gets a +1 from me.