View Single Post
Old 12th January 2017
e1-531g e1-531g is offline
VPN Cryptographer
 
Join Date: Mar 2014
Posts: 369
Default

@ocicat
Mathematically proven software often have not one, but a several of them. Each proof is about one thing.
A lot of your doubts are addressed by seL4's FAQ.
https://wiki.sel4.systems/FrequentlyAskedQuestions
https://sel4.systems/Info/FAQ/proof.pml

Mathematically proven software competes with high-assurance software. Software is used not only by laptops, smartphones and servers. There are also microcontrollers found in cars, planes. Software found in them is more stable (or at least should be because life depends on it and it is doable) than OpenBSD, Gnu/Linux, Windows and any other general-purpose operating system by a few orders of magnitude. There are people who know how to do it.

Of course verification of all OpenBSD code is beyond Project resources and I doubt that even biggest IT corporations could do that.
__________________
Signature: Furthermore, I consider that systemd must be destroyed.
Based on Latin oratorical phrase

Last edited by e1-531g; 12th January 2017 at 09:37 AM.
Reply With Quote