-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 Pierre THIERRY wrote: > Scribit Tom Bachmann dies 02/05/2006 hora 21:57: >>> OK. Now how many of these software carry formal proof of their >>> correctness? >> This is not true for the Hurd (afaik) > > Why? >
The TCB is more than just the kernel. To formally prove correctness like done with the kernel, the complete TCB would have to be written in bitc. I just didn't hear we want to do this. - -- - -ness- -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.2.2 (GNU/Linux) iD8DBQFEWP1fvD/ijq9JWhsRArWkAJ9vLM5kG44ADVAWNIy23oA1/1fM3QCfZfbK CbruuNxQZM7/kOFxXgjoWQo= =iN2f -----END PGP SIGNATURE----- _______________________________________________ L4-hurd mailing list [email protected] http://lists.gnu.org/mailman/listinfo/l4-hurd
