On Jul 29, 2014 6:14 PM, "Georgi Guninski" <guninski@guninski.com> wrote:
>
> >These proofs tie a meta-specification to the actual code. Look into the
> >sort of proofs they use. Basically they're saying "the code does what we
> >said it has to. Only if we accidentally told it to go skynet on us, it will
> >work perfectly". Things like segfaults would be pretty clearly not as
> >specified.
>
> By browsing the proofs, I have the impression
> they don't depend on the C code (and Isabelle
> parsing C appears not very trivial, though
> possible).
>
> If I backdoor the C code of the kernel, will
> the proof fail?

Isn't that the whole idea? It would really change the thing up if there's a backdoor!