The Coq mailing list

[Freek Wiedijk <freek AT cs.ru.nl>]

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