The Piano Test for Program Verification (2011)

Yep. Some people think "formal" means "mathematical," whereas it actually means "mechanical". A formal proof is one that can be correctly checked by a computer.

> The second problem is deeper: it is extremely difficult to argue convincingly that a verification result is correct. By “correct” I mean not only “mathematically sound” but also “the result is faithful to the intent of the verification effort.”

Worse. Even if we're convinced that the properties we verify are the right ones for correctness, we can only prove (even formally so) that an abstract algorithm satisfies them. We cannot prove that a system — which ultimately comprises a lot of hardware — does.

On the other hand, because reducing the probability of (catastrophic) failure is all we can hope for anyway, formal verification in various forms can help do that better — i.e., reduce the probability further, and with lower cost — than traditional testing methods alone. For example, because a formal specification can be quite short, it might be easier to convince ourselves that the properties we're checking are indeed the ones we're interested in than thousands of tests. I absolutely agree, though, that formal methods researchers often make the mistake on focusing on the wrong thing when communicating the value of their work. Formal methods can never prove a system correct, but they can help make it more correct and with less effort than using traditional assurance methods alone.

In other words, formal methods help catch some dangerous bugs more easily than traditional testing, and that is where their value is. Using the word "proof" when describing the goals of formal methods is doing them a disservice.

All verification makes assumption about some lower layer that is not itself verified.

For instance, you can't deduce the issues uncovered by Meltdown and Spectre from the semantics of the x86 instruction set architecture; so if you use that alone, you can falsely prove that x86 programs don't have security problems.

Rationally speaking, you shouldn't take any risk, however small, where there is no benefit. You wouldn't risk $1000 if the expected value from the entire risky event $900. If you're putting your life on the line, there has to be something in it other than convincing people that you really believe in something being correct.

Consider this: people have died for the sake of showing that their belief (e.g. religious) is correct! For instance, set themselves on fire or blown themselves up, or suffered as martyrs all the way to death. Just because some programmer put himself under the piano while his code was being fuzzed doesn't mean that it's correct, just that he or she is reckless and has a fanatical belief in the work. (If the programmer is reckless, I'm disinclined to believe in his or her code.)

Find a cybersecurity company that will indemnify you in case of breach or problem. (Hint, You won't.)

Skin in the game.

All we can prove is that some property holds. I think the major benefit is that it helps humans think about those properties and what is important. Especially in the world of computer systems it is impractical to expect a human to glance at a few thousands lines of code and spot where the race condition is. But if we simplify the model and check it with a computer it can usually find it rather fast.

Formal methods don't make systems inherently safer or fool-proof but they help us think about and understand complex systems. The name of the game after all is to not fool ourselves. The challenge is that we are the easiest ones to fool (paraphrasing Feynman here).

Yes, indeed. Life is infinite like the Sierpiński triangle, and at some point we deem the risks so small to fall within engineering tolerances. If only the code review engineers checking each change were as forgiving as the auditors.

Startups know this (business SWOT analysis). Hacker News knows this (karma). Some people like Elon Musk know this very well, so much that SpaceX is proud of their failures.

Humility is the source of integrity.