The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

If that is the service you want to provide, it's probably better to provide coqchk (which runs on .vo files) rather than coqc (which compiles .v files into .vo).  (Unfortunately .vo files are currently specific to the platform, OCaml version, and Coq version used to create them, but this problem should be fixable.). Unlike coqc, coqchk does not run plugin code and does not write to disk, so the only way you get arbitrary code execution is by finding a memory safety bug.  Furthermore, there are projects such as CertiCoq and the recent "Coq Coq Correct!" paper which make significant progress towards having a verified implementation of Coq's kernel (though I'm not sure if either project handles the module system yet, though).

So while currently I only trust coqc and coqchk for nonmalicious proofs, once it gets to the point that we can replace the guts of coqchk with a proven-correct implementation, then I'll mostly trust coqchk against even malicious proofs.  (I say mostly, because there are some parts of Coq, such as the guard checker and the module system and coinductives, where I either don't yet trust the theory to be free from inconsistencies, or where no one has even written up the theory, as far as I'm aware.)

On Sat, Feb 1, 2020, 21:51 Marco Servetto <marco.servetto AT gmail.com> wrote:

> Also: "put it in a container" doesn't address the other use case I mentioned above: namely, telling people that they can use Coq to certify the safety/correctness of untrusted code.

To make this more explicit:
if there was an online service that gives you "proven correct and safe code1"
and the corresponding coq proof code2; would running such proof be a
valid certification that such code1 is
correct and safe? or, is it possible that during the execution of
code2 arbitrary behavior makes a "yes" result even if the proof in
itself if bogus?
Note how running coq in a container or not does not really change the
issue here.