Why should it save labor. What it does is guarantee correctness which is like the holy grail for programmers. If you know shit's correct you can just assume stuff and it will actually work on the first try. You don't even need to write tests for it.
> What it does is guarantee correctness which is like the holy grail for programmers.
Formal verification can never guarantee correctness. For that to happen, you'd need to know that the property you verified is the property you want. If you have the ability to write correct specifications, you also have the ability to write correct programs, and running the verification doesn't add any value.
It guarantees correctness relative to a given requirement.
The real value of formal proofs lies in forcing you to think deeply about the requirement and your implementation of it and to make your assumptions about it explicit.
I have only ever used proof once in my career. We had a problem with an aircraft main computer that it was occasionally failing during start up and then refusing start again on all subsequent restarts. It was a multiprocessor computer and each processor was running start up tests some of which would interfere if run at the same time. I was worried that if the start-up was stopped at an arbitrary time it might leave the control variables in a state that would prevent further start-ups. I used Leslie Lamport's first technique (https://lamport.azurewebsites.net/pubs/pubs.html#proving) in an attempt to prove that it would always start up no matter at what point it was stopped the previous run. But I was unable to complete the proof in one situation. So I added a time delay to the start-up of some of the processors to ensure that this situation never occured. But that didn't fix the original problem. That turned out to be a hardware register being read before it had settled down. I fixed that later.
Correctness is taken to mean "The program matches its specification". Or, more literally, "the program is a correct implementation of it's specification".
Good software, even with bugs, released today, can be used today. Perfect software, released two years from now, cannot be used today, or next week, or next year. "Good now" beats "perfect later", at least now, but often it beats it later too.
While someone is working on "provably perfect", someone who isn't using that approach has released four versions that were not perfect, but were good enough to be useful. That person took the market, and when the provably perfect version finally comes out, nobody cares, because they're used to how the other one works, and it has more features. And if the "provably perfect" person wants to implement those features, they have to change the program, which means they have to re-do the proof...
Also "perfect software" doesn't actually mean "perfectly robust systems" - at the end of the day it has to interact with the Real World, and the Real World is messy. You still have to cope with failures from cosmic rays, power brownouts, hardware bugs (or at least a difference in specification of the hardware to the model used for this sort of formal verification), failures communicating with other devices etc.
So critical software already has to deal with failures and recover, no amount of formal verification will remove that requirement.
But you don't have to do the proving. You can let someone who is, like, REALLY good at formal verification do it and then benefit from the libraries they produce
Verification is useful when you're dealing with low level or very declarative stuff. You don't really have to "verify" a CRUD repository implementation for a random SPA. But the primitives it relies on, it would be good if those were verified.
thaumasiotes|1 year ago
Formal verification can never guarantee correctness. For that to happen, you'd need to know that the property you verified is the property you want. If you have the ability to write correct specifications, you also have the ability to write correct programs, and running the verification doesn't add any value.
tristramb|1 year ago
The real value of formal proofs lies in forcing you to think deeply about the requirement and your implementation of it and to make your assumptions about it explicit.
I have only ever used proof once in my career. We had a problem with an aircraft main computer that it was occasionally failing during start up and then refusing start again on all subsequent restarts. It was a multiprocessor computer and each processor was running start up tests some of which would interfere if run at the same time. I was worried that if the start-up was stopped at an arbitrary time it might leave the control variables in a state that would prevent further start-ups. I used Leslie Lamport's first technique (https://lamport.azurewebsites.net/pubs/pubs.html#proving) in an attempt to prove that it would always start up no matter at what point it was stopped the previous run. But I was unable to complete the proof in one situation. So I added a time delay to the start-up of some of the processors to ensure that this situation never occured. But that didn't fix the original problem. That turned out to be a hardware register being read before it had settled down. I fixed that later.
rocqua|1 year ago
AnimalMuppet|1 year ago
Good software, even with bugs, released today, can be used today. Perfect software, released two years from now, cannot be used today, or next week, or next year. "Good now" beats "perfect later", at least now, but often it beats it later too.
While someone is working on "provably perfect", someone who isn't using that approach has released four versions that were not perfect, but were good enough to be useful. That person took the market, and when the provably perfect version finally comes out, nobody cares, because they're used to how the other one works, and it has more features. And if the "provably perfect" person wants to implement those features, they have to change the program, which means they have to re-do the proof...
kimixa|1 year ago
So critical software already has to deal with failures and recover, no amount of formal verification will remove that requirement.
unification_fan|1 year ago
Verification is useful when you're dealing with low level or very declarative stuff. You don't really have to "verify" a CRUD repository implementation for a random SPA. But the primitives it relies on, it would be good if those were verified.
twinkjock|1 year ago