Long division verified via Hoare logic
cofault.com
Long division verified via Hoare logic
1–10 of 63 posts
Re: Long division verified via Hoare logic
#2i think this shows why formal verification, while certainly useful in specialized situations, will likely not be a major boost for software productivity[1]
[1] - https://worrydream.com/refs/Brooks_1986_-_No_Silver_Bullet.p...:
> I do not believe we will find the magic here. Program verification is a very powerful concept, and it will be very important for such things as secure operating system kernels. The technology does not promise, however, to save labor. Verifications are so much work that only a few substantial programs have ever been verified
Re: Long division verified via Hoare logic
#3i think this shows why formal verification, while certainly useful in specialized situations, will likely not be a major boost for software productivity[1] [1] - https://worrydream.com/refs/Brooks_1986_-_No_Silver_Bullet.p... : > I do not believe we will find the magic here. Program verification is a very powerful concept, and it will be very important for such things as secure operating system kernels. The technolog…
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.
Re: Long division verified via Hoare logic
#4i think this shows why formal verification, while certainly useful in specialized situations, will likely not be a major boost for software productivity[1] [1] - https://worrydream.com/refs/Brooks_1986_-_No_Silver_Bullet.p... : > I do not believe we will find the magic here. Program verification is a very powerful concept, and it will be very important for such things as secure operating system kernels. The technolog…
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.
This is why connecting formal verification to an infinite (possibly-incorrect-)labor machine such as an LLM system can indeed save human labor.
Re: Long division verified via Hoare logic
#5i think this shows why formal verification, while certainly useful in specialized situations, will likely not be a major boost for software productivity[1] [1] - https://worrydream.com/refs/Brooks_1986_-_No_Silver_Bullet.p... : > I do not believe we will find the magic here. Program verification is a very powerful concept, and it will be very important for such things as secure operating system kernels. The technolog…
True, but also the work can be reduced significantly with better tooling, which is still being developed but has improved markedly over the past decade. Eg SMT solvers that can output proofs, or tactics in Coq or Lean.
I'm hoping that this will be a big application of AI actually. If an AI can be built do to this simple but very tedious work, and your verification tool is capable of catching any errors it makes, then you've covered up a major flaw of formal verification (its tediousness) and of AI (its tendency to output bullshit).
Re: Long division verified via Hoare logic
#6i think this shows why formal verification, while certainly useful in specialized situations, will likely not be a major boost for software productivity[1] [1] - https://worrydream.com/refs/Brooks_1986_-_No_Silver_Bullet.p... : > I do not believe we will find the magic here. Program verification is a very powerful concept, and it will be very important for such things as secure operating system kernels. The technolog…
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.
Because it takes so much work.
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...
Re: Long division verified via Hoare logic
#7Earlier quoted context omitted.
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.
Because it takes so much work . 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…
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.
Re: Long division verified via Hoare logic
#8i think this shows why formal verification, while certainly useful in specialized situations, will likely not be a major boost for software productivity[1] [1] - https://worrydream.com/refs/Brooks_1986_-_No_Silver_Bullet.p... : > I do not believe we will find the magic here. Program verification is a very powerful concept, and it will be very important for such things as secure operating system kernels. The technolog…
True, but also the work can be reduced significantly with better tooling, which is still being developed but has improved markedly over the past decade. Eg SMT solvers that can output proofs, or tactics in Coq or Lean. I'm hoping that this will be a big application of AI actually. If an AI can be built do to this simple but very tedious work, and your verification tool is capable of catching any errors it makes, then…
Proving safety is just a small part of the problem to be solved. The hard part is actually structuring the program such that its correctness can even be formulated as a formal property which can be proved. For a lot of software that alone is highly nontrivial.
Re: Long division verified via Hoare logic
#9Earlier quoted context omitted.
True, but also the work can be reduced significantly with better tooling, which is still being developed but has improved markedly over the past decade. Eg SMT solvers that can output proofs, or tactics in Coq or Lean. I'm hoping that this will be a big application of AI actually. If an AI can be built do to this simple but very tedious work, and your verification tool is capable of catching any errors it makes, then…
Proving safety is just a small part of the problem to be solved. The hard part is actually structuring the program such that its correctness can even be formulated as a formal property which can be proved. For a lot of software that alone is highly nontrivial.
From "No Silver Bullet":
> More seriously, even perfect program verification can only establish that a program meets its specification. The hardest part of the software task is arriving at a complete and consistent specification, and much of the essence of building a program is in fact the debugging of the specification
Re: Long division verified via Hoare logic
#10Earlier quoted context omitted.
Because it takes so much work . 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…
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 cr…
And unexpected input from other systems. And if it was unexpected in a way that wasn't covered by your proof, then your program is not guaranteed to work correctly on that input. And the real world has a lot of ways for input to do unexpected things...