What does Zig Forums think about seL4?

Yeah user is right here 2. Anything can be proven if you don't do termination checking. Whiley is clearly in inferior limited use /power system.

If we cannot trust any machine to follow a mathematical verification process, then there's no point in using computers for mathematical verification. All forms of cryptography are unreliable an we may as well post our personal banking details in the open for all to see.

you give up easily user

Mods, we need a fucking medal over here

All I'm saying is that I trust the automated formal verification of a particular binary program without the need to formally verify every other part of the computer doing the verifying. I trust this because I believe in input-process-output for the verification and assume that this will be equally the same for all computers.

Well user trust is not proof :^).

The more i think about it, the more I wonder if it will be adopted inside mobile basebands (and other consumer products) like earlier versions of L4 were, or if it will end up being a defense-contractor interface to a shoddy C++ tactical webserver.

Every single shitcoin has claimed "mathematical proof" and then had flaws revealed, I'm not impressed.

Attached: Sure Anon.jpg (254x254, 29.07K)

Mathematical proof only means that the process is mathematically consistent. Having a formal proof doesn't imply the system is any good for its purpose. To find if it's good for its purpose, you have to implement the system and test it out.