3 ms·

The idea of formal verification of code is kafkaesque. Its popularity is proportional to the inefficiency and irrationality of the economic system within which

The idea of formal verification of code is kafkaesque. Its popularity is proportional to the inefficiency and irrationality of the economic system within which it exists. Code is an expression of pure logic. So if there is any incorrect assumption or flaw in that logic, it can be verified by simply reading the code. Given that premise, the usefulness of formal verification can be disproved in a single English sentence: Formal verification does not remove the element of human error from a system; it removes it from the code and adds it to the system of proofs which verify that code... Proofs can be written with incorrect assumptions (human error) in the same way that code can be written with incorrect assumptions. As one of the people in the article acknowledges, writing good proofs is challenging; "challenging" inescapably means "prone to human error". Formal verification proponents seem to have conveniently forgotten to apply formal verification to prove the effectiveness of formal verification. The great irony of this article is that it attempts to rely on exhaustive proof (which is the basis of unit testing) to prove the effectiveness of formal proof - I.e. we tested formal verification with that helicopter that one time and the hackers couldn't hack it for 6 months, therefore formal proof is effective - That's a lousy unit test case and it doesn't prove formal verification.

docandrew 7y ago
The difference is that code with bugs can still compile, but proofs that are unsound won't check. Now granted, you can still prove the wrong thing or _not_ prove the thing that is supposed to make your system robust is taking place, so it's still very much a human endeavor with all that entails. I think a dedicated red team going after a system for 6 months and not finding anything is a pretty good "unit test", personally. It's _evidence_ of effectiveness, not _proof_.
tgflynn 7y ago
> Formal verification does not remove the element of human error from a system; it removes it from the code and adds it to the system of proofs which verify that code... Proofs can be written with incorrect assumptions (human error) in the same way that code can be written with incorrect assumptions. As one of the people in the article acknowledges, writing good proofs is challenging; "challenging" inescapably means "prone to human error". I think those statements are rather inaccurate, or at a minimum prone to erroneous interpretations. Formal verification is usually based on machine checked proofs. It doesn't matter how much error occurs in the creation of a proof, once it is checked it is known to be a valid proof with mathematical certainty. That does depend on the correctness of the proof checker, but in principle that can be formally verified as well. I think the main issues with formal verification lie elsewhere than where you seem to be placing them. Such as the problem that the specification itself may be incomplete or contain errors.

docandrew 7y ago

The difference is that code with bugs can still compile, but proofs that are unsound won't check. Now granted, you can still prove the wrong thing or _not_ prove the thing that is supposed to make your system robust is taking place, so it's still very much a human endeavor with all that entails. I think a dedicated red team going after a system for 6 months and not finding anything is a pretty good "unit test", personally. It's _evidence_ of effectiveness, not _proof_.

tgflynn 7y ago

> Formal verification does not remove the element of human error from a system; it removes it from the code and adds it to the system of proofs which verify that code... Proofs can be written with incorrect assumptions (human error) in the same way that code can be written with incorrect assumptions. As one of the people in the article acknowledges, writing good proofs is challenging; "challenging" inescapably means "prone to human error". I think those statements are rather inaccurate, or at a minimum prone to erroneous interpretations. Formal verification is usually based on machine checked proofs. It doesn't matter how much error occurs in the creation of a proof, once it is checked it is known to be a valid proof with mathematical certainty. That does depend on the correctness of the proof checker, but in principle that can be formally verified as well. I think the main issues with formal verification lie elsewhere than where you seem to be placing them. Such as the problem that the specification itself may be incomplete or contain errors.