[Cryptography] Formal Verification (was Re: Trust & randomness in computer systems)

[Peter Gutmann]

Perry E. Metzger <perry at piermont.com> writes:

>I will also point out that mere model checking isn't the state of the art --
>we can now do far better. CompCert, for example, is written completely in Coq
>and then extracted into OCaml.

Which leads to a variant of the Gnu problem in which, to build Gnu-anything,
you first need Gnu-everything-else.  I started playing with the CompCert
rabbit hole a few days ago when you first mentioned it, but now I'm waiting
for the proverbial rainy weekend to keep going...

Peter.