The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

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