The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

On 30/09/15 17:44, Freek Wiedijk wrote:
> On the CakeML developers mailing list, there was a mention of:
> <http://gallium.inria.fr/blog/coq-eval/>
> Then Magnus wrote; 
> [...]
>     I wonder what the trust issues are when computing with the
>     VM/native mode within Coq. The jumps into and out of the VM/native
>     mode sound scary regarding the trust story of the prover. Are
>     these VM/native-mechanisms in fact not trusted and somehow
>     cleanly separated from the trusted part of Coq's kernel?

Normally, I'd let the authors of vm_compute and native_compute reply,
but they are probably busy pumping water off their basements...
(Big floods near Sophia-Antipolis recently.)

The principles underlying vm_compute (the strong reduction strategy
and the compilation scheme to VM code) were formalized and verified in
Coq by Benjamin Grégoire in his PhD thesis.  The actual implementation
of vm_compute is not formally verified, though, and, yes, it is part
of the trusted kernel.  Empirically, based on the rate of discovery of
proofs of False, it looks as reliable as the rest of the Coq
implementation.

This said, the experiment I mentioned in my blog post (execute
CompCert within Coq using vm_compute) doesn't aim at 100% formal
confidence of the CakeML kind.  Instead, it just aims at an alternate
execution mechanism for CompCert that is independent from Coq's
extraction and OCaml's compilation of the extracted code.  In the
context of software certification using a combination of tests and
formal methods, the existence of two independent implementations that
produce the same results already has some certification value, not as
high as a full formal verification, but not negligible either.
(Motto: "if something is true for two independent reasons, that makes
it more true!").

Bas Spitters adds:

> There are at least to projects trying to improve the level of trust:
> http://www.maximedenes.fr/download/coqonut.pdf
> https://www.cs.princeton.edu/~appel/certicoq/

The Coqonut project (by Maxime Dénès and I) aims at equipping Coq with
an evaluation mechanism that is both more efficient and more
trustworthy than vm_compute and native_compute, via a
formally-verified JIT compiler from Gallina to x86-64.  The project is
at an early stage and we're lacking time and manpower to make it
progress as fast as we'd like, so don't hold your breath.

- Xavier Leroy