←back to thread

Systems Correctness Practices at AWS: Leveraging Formal and Semi-Formal Methods

(queue.acm.org)
167 points yarapavan | 2 comments | 01 Apr 25 14:59 UTC | HN request time: 0s | source
Show context
gqgs ◴[01 Apr 25 19:17 UTC] No.43550402[source]▶
A key concern I've consistently had regarding formal verification systems is: how does one confirm the accuracy of the verifier itself?

This issue appears to present an intrinsically unsolvable problem, implying that a formally verified system could still contain bugs due to potential issues in the verification software.

While this perspective doesn't necessarily render formal verification impractical, it does introduce certain caveats that, in my experience, are not frequently addressed in discussions about these systems.

replies(8): >>43550610 #>>43550706 #>>43550740 #>>43552467 #>>43553529 #>>43553826 #>>43554265 #>>43558410 #
ninetyninenine ◴[02 Apr 25 05:10 UTC] No.43553826[source]▶
This is not just a problem with formal verification systems. It's a problem intrinsic to math, science and reality.

We call these things axioms. The verifier must be assumed to be true.

For all the axioms in mathematics... we don't know if any of those axioms are actually fully true. They seem to be true because we haven't witnessed a case where they aren't true. This is similar to how we verify programs with unit tests. For the verifier it's the same thing, you treat it like an axiom you "verify" it with tests.

replies(1): >>43554718 #
1. gqgs ◴[02 Apr 25 08:36 UTC] No.43554718[source]▶
I believe there is a distinction between those concepts.

Axioms are true by their own definition. Therefore, discovering an axiom to be false is a concept that is inherently illogical.

Discovering that a formal verification system produced an incorrect output due to a bug in its implementation is a perfectly well-defined concept and doesn't led to any logical contradictions; unless you axiomatically define the output of formal verification systems to be necessarily correct.

I believe this definition don't make sense in the general case considering the number of vectors that can introduce errors into software.

replies(1): >>43556225 #
2. ninetyninenine ◴[02 Apr 25 13:04 UTC] No.43556225[source]▶
Being true by definition is just assigning something to be true by assumption.

Who makes a definition? Are definitions intrinsic to reality? No. Definitions are made up concepts from language which is also another arbitrary made up thing. When something is defined to be an axiom the human is making something up and arbitrarily assigning truth to that concept.

> I believe this definition don't make sense in the general case considering the number of vectors that can introduce errors into software.

You’re making up a definition here. Which is the same as an axiom.

Your question is what verifies the verifier? But that question is endless because what verifies the verifier of the verifier? It’s like what proves the axiom? And what proves the proof of the axiom?

The verifier defines the universe of what is correct and what is incorrect. It is the axiom. It is an assumption at its core. You can pretty it up by calling it a more advanced thing like “definition” but in the end it is the exact same thing as assuming and making up a fact that something is true without any proof.