The Coq mailing list

[Timothy Carstens <intoverflow AT gmail.com>]

Thanks! That might work; I already wanted to use github.com/ejgallego/jscoq in browser; I haven't checked yet, but if it could give me .vo bytestreams I'd be good to go.

I was also thinking about running jscoq in Node on the backend. That doesn't solve any problems on its own, but it would give me a few layers (such as libuv) where I could reliably catch system calls. Presumably the ocaml platform has something similar but I'm less familiar with its internals. I'll think some more on whether or not there might be a cleaner way to achieve this - let me know if anyone has any suggestions.

Bigger picture:

I'm extremely optimistic about the direction the Coq ecosystem is going.

I think I mentioned earlier that I know everyone is super busy and I recognize that my particular ask isn't a high priority at the moment.

I'm not worried about it long term; many years ago I had stronger concerns, but I've seen some of the changes that have taken place since then. The progress has been outstanding. And even though it's inconvenient for my hypothetical project, I'd rather folks continue their current improvement efforts instead of worrying about this thread.

CertiCoq and "Coq Coq Correct!", in particular, have me very excited. To me, they both represent a drastic maturation of the Coq ecosystem and are sure to open up lots of excellent avenues for integrating Coq and Coq artifacts into other projects.

-t

On Sat, Feb 1, 2020 at 7:45 PM Jason Gross <jasongross9 AT gmail.com> wrote:

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.