Alleged "microkernel mathematically proven to be bug free"

Georgi Guninski guninski at guninski.com
Tue Jul 29 05:41:38 PDT 2014


I didn't spend much time on this, just browsed
some proofs. The proofs appear to not depend to
on the C code AFAICT. Would trojanizing the C
code invalidate the proofs?

The haskell stuff appear to not contain all
info about the C code.

On Mon, Jul 28, 2014 at 06:26:50PM +0300, Georgi Guninski wrote:
> news:
> http://www.theregister.co.uk/2014/07/28/aussie_droneprotecting_hackerdetecting_kernel_goes_open_source/
> site:
> http://sel4.systems/
> 
> AFAICT they used Isabelle for the proofs.
> 
> Coq sucks much (not counting its developers).



More information about the cypherpunks mailing list