The Coq mailing list

[Epiphanie <landeguy AT gmail.com>]

> Empirically, based on the rate of discovery of
> proofs of False, it looks as reliable as the rest of the Coq
> implementation.
I am not quite sur I understand that sentence, given there is at least
two known proof of false in vm_compute (that are still present in the
current stable release but not the beta, as far as I know), notably one
using 256 constructor for one object.
Perhaps I do not understand the aim of vm_compute, but shouldn't it
display a warning when used? Since I thought the aim of Coq was to have
a complete automatisation of certified proof.
Thank you very much,
Epiphanie

Le 08/10/2015 17:34, Maxime Dénès a écrit :
> Not much to add to Xavier's answer, except that vm_compute and
> native_compute have a special status regarding trust in Coq's
> distribution: they are not included in Coq's checker (coqchk).
>
> I guess this was motivated by keeping the core TCB relatively small in
> terms of lines of code. However, as pointed out by Xavier, empirical
> data seem to indicate that these parts of the kernel are not less
> trustworthy than others.
>
> Also, these facilities are meant to be used when the regular interpreter
> is not efficient enough. Used this way, they allow users to certify
> computations that would otherwise remain unverified, actually increasing
> confidence :)
>
> Finally, one can know by inspecting a term if the VM or the native
> compiler were used to typecheck it. We may one day provide a
> fine-grained command that given a proof would tell the user what TCB
> needs to be trusted.
>
> Maxime.
>
> On 10/06/2015 07:09 PM, Xavier Leroy wrote:
>> 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
>