The Coq mailing list

["Andrew W. Appel" <appel AT CS.Princeton.EDU>]

Regarding the Certicoq project,

https://www.cs.princeton.edu/~appel/certicoq/

Our research focus at present is to build a proved-correct 
extracter/compiler
for application outside Coq.  In essence, it would provide a verified
replacement for the current Coq extraction program (which is an
unverified OCaml program), the current OCaml compiler (which is
an unverified OCaml program), and the current OCaml runtime (which
is an unverified C program).

But (at present), we are not building a replacement for vm_compute
or native_compute inside Coq.

-- Andrew Appel

On 9/30/2015 3:41 PM, Bas Spitters wrote:
> 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/
>
> I'll leave it to the people involved to say more.
>
> On Wed, Sep 30, 2015 at 5:44 PM, Freek Wiedijk 
> <freek AT cs.ru.nl>
>  wrote:
> > Dear all,
> >
> > On the CakeML developers mailing list, there was a mention of:
> >
> > <http://gallium.inria.fr/blog/coq-eval/>
> >
> > Then Magnus wrote;
> >
> >      Interesting! So Xavier Leroy can run CompCert inside Coq at about
> >      15 % of normal speeds, which of course is much better than we can
> >      hope for with EVAL in HOL4.
> >
> >      I'd love to have fast evaluation mechanisms in HOL4. However,
> >      support for evaluation in a VM/native mode would require
> >      *significant* modifications to HOL4's trusted kernel...
> >
> >      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?
> >
> > And then I wondered how people on the Coq list feel about this,
> > and got permission from Magnus to repost his message here.
> >
> > Freek