No hardware failure is considered? No cosmic rays flipping bits? No soft or hard real-time guarantees are discussed? What about indeterminate operations that can fail such as requesting memory from some operating system dynamically?
I'm asking because I thought high integrity systems are generally evaluated and certified as a combination of hardware and software. Considering software alone seems pretty useless.
Many interesting statements aren't a property of the code alone. They're a property of the code when it's run in a particular environment. If you want the proof to be portable then it should only make assumptions that are true in any environment.
Formal verification is ultimately an epistemological problem, how do we know that our model of reality corresponds to reality?
People have commented that validation is different from verification, but I think validation can be done by formally specifying the environment the program runs in.
For example, the question whether user can do X in your software corresponds to a question, is there a sequence of user inputs such that the software plus operating system leads to the output X.
By including the environment (like the operating system) into the formal spec we could answer (in theory) such questions.
Even if the question is fuzzy, we can today formalize it with AI models. For example, if we ask, does paint program allow user to draw a rose? We can take a definition of a rose from a neural network that recognizes what a rose is, and formally verify the system of paint program and rose verifier given by the NN.
Definition by consensus doesn't always equal absolute definition, to continue your epistemological metaphor. Just because the consensus states it's a rose doesn't mean it absolutely is in the truest sense (the artist, program, and neural network consensus could all be wrong in some intrinsic way).
From a quick look at it, it seems to be a "case 1" potential error, as the proof is done by hand. That is the warning is likely because it is a mathematical exercise first, and the code is for illustration and not for inclusion in production software.
> I wrote that the "binary search" bug happened because they proved the wrong property, but you can just as well argue that it was a broken assumption (that integers could not overflow).
No, you can't argue that (well, argue that successfully). If you are trying to prove some properties of a program X written in a certain programming language Y, you can't "just assume" that the semantics of Y are different from what they are! The integers do overflow in Java, that's explicitly stated in the Java's spec.
The article did not also point out issues like the compiler or interpreter having a runtime error, the hardware the software is running on having a defect, etc.
Do we consider these out of scope of the discussion?
There's this place for formal proving that most people won't get to and think it's stupid. I was such person some time ago, but then started to work on the system that: Required 2-3 months for implementation, had no room for error, made processing mistakes cost in thousands of Euros (even silly things). Than you start to wonder "hmmm... how can I use something better than just good practices and judgement? How can I _prove_ design A works".
And usually there are tangible problems to avoid: Ensuring that money won't get lost in transaction. Making sure that legal paperwork will be delivered or returned on time. Or that CSV file costing arm and leg for a single row won't have more rows than necessary. Many of these problems are borderline paradoxical. It's known that (as with Two Generals) there are no complete solutions. Usually it's like playing a catch with reality. A game that goes "what happens if we duplicate money mid-flight?" - "which system is source of truth in case of fraud", "do we rather risk false negative or accept MIA state" etc.
Sure, it's fun to model a crossroad with streetlights and a chicken just for kicks, but the main "why?" for formal proving is having "this design is good because I've seen the proof of it" moment.
But what kind of questions are asked is just as important. I can bet asbestos met all the standards it was checked against :)
You're touching on a timeless approach which is currently not possible, given the limits of reality. You'd need to know for a fact all potential outlays in order to make sure every change your program (creation) creates is accounted for and proved against. Since you do not have perfect information, your proof, by current definition, cannot be proved to be perfect.
That's true, just as I cannot possibly measure car speed given innate measuring error which is not a defense from getting a speeding ticket.
Formal proving isn't about getting to "my model is reality" but having step above mere imagination or educated guess. That's why it's possible to model paradoxical models. Given N systems they all can fail at the same time and there's nothing that can be done to guarantee message RECV+ACK. So at some point there's invariant saying "ok, we say that 3 out of 5 systems will always work". If you break invariant all hell is loose but at that point many weird stuff might happen.
Usually when one needs to think about message passing in a way like [0] formal proving can save lives (or bottoms, depending on the context).
"The assumptions are wrong" is an unsatisfying "catch-all": compiler, hardware, environment, concurrency bugs.
Here's one that's been bugging me lately: Dekker's algorithm (mutual exclusion / critical section) won't work on modern hardware. CPUs are free to rearrange reads and writes such that they still make sense under single-threaded conditions.
It's kind of put me off learning about lockfree/lockless programming. Even if I make a machine-checked proof that my concurrent code races only in acceptable ways, I have no way of knowing which instructions will be re-ordered, invalidating the proof.
21 comments
[ 2.1 ms ] story [ 38.8 ms ] threadI'm asking because I thought high integrity systems are generally evaluated and certified as a combination of hardware and software. Considering software alone seems pretty useless.
verification - Are we building the software right?
validation - Are we building the right software?
makes many a thing easier to talk about at work
Why not just use an assertion? It costs more at runtime, but it's far less dev time than developing a proof, right?
People have commented that validation is different from verification, but I think validation can be done by formally specifying the environment the program runs in.
For example, the question whether user can do X in your software corresponds to a question, is there a sequence of user inputs such that the software plus operating system leads to the output X.
By including the environment (like the operating system) into the formal spec we could answer (in theory) such questions.
Even if the question is fuzzy, we can today formalize it with AI models. For example, if we ask, does paint program allow user to draw a rose? We can take a definition of a rose from a neural network that recognizes what a rose is, and formally verify the system of paint program and rose verifier given by the NN.
There was some meta-bug with encoding which almost is like an internal joke but I don't think it's intentional. The Haskell code examples have:
several times, and that `>` entity should very likely just be a `<` in the source code."Beware of bugs in the above code; I have only proved it correct, not tried it." - Donald Knuth
Source: https://staff.fnwi.uva.nl/p.vanemdeboas/knuthnote.pdf
From a quick look at it, it seems to be a "case 1" potential error, as the proof is done by hand. That is the warning is likely because it is a mathematical exercise first, and the code is for illustration and not for inclusion in production software.
No, you can't argue that (well, argue that successfully). If you are trying to prove some properties of a program X written in a certain programming language Y, you can't "just assume" that the semantics of Y are different from what they are! The integers do overflow in Java, that's explicitly stated in the Java's spec.
And usually there are tangible problems to avoid: Ensuring that money won't get lost in transaction. Making sure that legal paperwork will be delivered or returned on time. Or that CSV file costing arm and leg for a single row won't have more rows than necessary. Many of these problems are borderline paradoxical. It's known that (as with Two Generals) there are no complete solutions. Usually it's like playing a catch with reality. A game that goes "what happens if we duplicate money mid-flight?" - "which system is source of truth in case of fraud", "do we rather risk false negative or accept MIA state" etc.
Sure, it's fun to model a crossroad with streetlights and a chicken just for kicks, but the main "why?" for formal proving is having "this design is good because I've seen the proof of it" moment.
But what kind of questions are asked is just as important. I can bet asbestos met all the standards it was checked against :)
Formal proving isn't about getting to "my model is reality" but having step above mere imagination or educated guess. That's why it's possible to model paradoxical models. Given N systems they all can fail at the same time and there's nothing that can be done to guarantee message RECV+ACK. So at some point there's invariant saying "ok, we say that 3 out of 5 systems will always work". If you break invariant all hell is loose but at that point many weird stuff might happen.
Usually when one needs to think about message passing in a way like [0] formal proving can save lives (or bottoms, depending on the context).
[0]: https://xlii.space/eng/network-scenarios/
Here's one that's been bugging me lately: Dekker's algorithm (mutual exclusion / critical section) won't work on modern hardware. CPUs are free to rearrange reads and writes such that they still make sense under single-threaded conditions.
It's kind of put me off learning about lockfree/lockless programming. Even if I make a machine-checked proof that my concurrent code races only in acceptable ways, I have no way of knowing which instructions will be re-ordered, invalidating the proof.