Re: Alleged "microkernel mathematically proven to be bug free"

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_hackerdetecti... site: http://sel4.systems/

AFAICT they used Isabelle for the proofs.

Coq sucks much (not counting its developers).