The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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.