Re:Why you should, actually, rewrite some of it in Rust
by AnimalMuppet on Wednesday July 12, 2017 @12:33PM
(#14753952)
Worse: "It's amazing how many bugs there can be in a formally verified piece of software." I forget who said it, but it's been a long time. (Maybe in connection with formal verification of an OS? Does anyone remember?)
Formal verification only works if the formal verification was mistake-free. (And how are you going to prove that? With a formal verification? It's turtles all the way down...) Also, it only works for the aspects that were formally verified. Heartbleed, for example, could be regarded as a flaw in the specification; formally verifying that the code matches the spec won't save you from that.
Formal verification only works if the formal verification was mistake-free. (And how are you going to prove that? With a formal verification? It's turtles all the way down...) Also, it only works for the aspects that were formally verified. Heartbleed, for example, could be regarded as a flaw in the specification; formally verifying that the code matches the spec won't save you from that.