←back to thread

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

(queue.acm.org)
167 points yarapavan | 1 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 #
1. csbartus ◴[01 Apr 25 19:58 UTC] No.43550740[source]▶
Perhaps there is no such thing like absolute truth.

In category theory / ologs, a formal method for knowledge representation, the result is always mathematically sound, yet ologs are prefixed with "According to the author's world view ..."

On the other way truth, even if it's not absolute, it's very expensive.

Lately AWS advocates a middle ground, the lightweight formal methods, which are much cheaper than formal methods yet deliver good enough correctness for their business case.

In the same way MIT CSAIL's Daniel Jackson advocates a semi-formal approach to design likely-correct apps (Concept design)

It seems there is a push for better correctness in software, without the aim of perfectionism.