3 ms·

To me, this is the argument for formal verification. I don't want to hear a hand-waving explanation that this algorithm will always complete. If the algorithm i

To me, this is the argument for formal verification. I don't want to hear a hand-waving explanation that this algorithm will always complete. If the algorithm is sufficiently complex I want proof. Otherwise, why would I believe you? Abstractions, in the mathematical sense, always hold (unless there is a flaw in the definition itself). Axioms in any sense are always going to throw a wrench in things. Thank Godel. But that shouldn't mean we cannot make progress. Do the work, show your proof! Think hard! Although sometimes all you need are a few unit tests. They key is to develop the wisdom to know when unit tests aren't sufficient for the task at hand.

bee_rider 2y ago
I dunno. Even in some fairly math-y situations, line solving sparse linear systems, we get stuff like BiCGStab which often will work well and converge in cases where we can’t prove that it must. CS seems mostly good for proving that everything is hopeless in the rigorous general case and, hey, here are some heuristics to give you hope again.
atrus 2y ago
> Abstractions, in the mathematical sense, always hold (unless there is a flaw in the definition itself). Axioms in any sense are always going to throw a wrench in things. Thank Godel. But that shouldn't mean we cannot make progress. But this seems like an argument against formal verification. Formal verification is 100x harder than writing tests...and still doesn't guarantee correctness? Those axiom wrenches are still there, those flaws in the definition are still there, not to mention the flaws in the proof writing. All that extra effort for what gain?
- agentultra 2y ago
  It guarantees correctness vis. the axioms chosen. That's a much more powerful statement and guarantee than a unit test which only exercises a single example. A formal proof that an algorithm makes progress, doesn't require a lock, or whatever property the proof is arguing is 100% guaranteed for every case. For example, a simple function over the set of integers. A unit test can only test individual elements of the set. A proof demands more: the property must hold over all elements of the set. The Incompleteness Theorem puts a limit on the provability. That hasn't stopped mathematicians from pursuing the formalization of mathematics. It shouldn't stop computer scientists and programmers either. In fact it tends to make us more honest about the limits and capabilities of our systems.
  - senkora 2y ago
    Agreed. A good set of unit tests partitions the input space into parts, and then provides an existence proof that the program is correct for an example chosen from each part. A good formal proof does the same, but provides a universal proof that the program is correct for all examples chosen from each part. Both strategies can fail if they miss an important part of the input set. Unit tests can also fail if a program is “adversarial” and fails in a specific input that isn’t the particular example. In practice, achieving “a good set of unit tests” requires you to mentally work out how to partition the input set in a way that matches your program, and at that point you’re most of the way to proving it correct, so you might as well do that. It still might make sense to write unit tests if you don’t have the tooling to enforce a mechanical proof.
mbonnet 2y ago
Formal verification is nice, but requires crazy skilled people at high cost. It's not always practical/feasible to have as part of your SWE process.
- agentultra 2y ago
  And it's not necessary for every project. It's nice to have when it is though. The cost is coming down. Proof automation is incredible today and rapidly improving. This is the part that does the tedious parts of a proof for you so that you can focus on the theorems that matter. The languages and proof systems themselves are easier than ever to pick up and use which is bringing the skill cost down. I don't think most software projects need a huge, dedicated team of specialists to benefit from formal software verification.

bee_rider 2y ago

I dunno. Even in some fairly math-y situations, line solving sparse linear systems, we get stuff like BiCGStab which often will work well and converge in cases where we can’t prove that it must. CS seems mostly good for proving that everything is hopeless in the rigorous general case and, hey, here are some heuristics to give you hope again.

atrus 2y ago

> Abstractions, in the mathematical sense, always hold (unless there is a flaw in the definition itself). Axioms in any sense are always going to throw a wrench in things. Thank Godel. But that shouldn't mean we cannot make progress. But this seems like an argument against formal verification. Formal verification is 100x harder than writing tests...and still doesn't guarantee correctness? Those axiom wrenches are still there, those flaws in the definition are still there, not to mention the flaws in the proof writing. All that extra effort for what gain?

agentultra 2y ago
It guarantees correctness vis. the axioms chosen. That's a much more powerful statement and guarantee than a unit test which only exercises a single example. A formal proof that an algorithm makes progress, doesn't require a lock, or whatever property the proof is arguing is 100% guaranteed for every case. For example, a simple function over the set of integers. A unit test can only test individual elements of the set. A proof demands more: the property must hold over all elements of the set. The Incompleteness Theorem puts a limit on the provability. That hasn't stopped mathematicians from pursuing the formalization of mathematics. It shouldn't stop computer scientists and programmers either. In fact it tends to make us more honest about the limits and capabilities of our systems.
- senkora 2y ago
  Agreed. A good set of unit tests partitions the input space into parts, and then provides an existence proof that the program is correct for an example chosen from each part. A good formal proof does the same, but provides a universal proof that the program is correct for all examples chosen from each part. Both strategies can fail if they miss an important part of the input set. Unit tests can also fail if a program is “adversarial” and fails in a specific input that isn’t the particular example. In practice, achieving “a good set of unit tests” requires you to mentally work out how to partition the input set in a way that matches your program, and at that point you’re most of the way to proving it correct, so you might as well do that. It still might make sense to write unit tests if you don’t have the tooling to enforce a mechanical proof.

mbonnet 2y ago

Formal verification is nice, but requires crazy skilled people at high cost. It's not always practical/feasible to have as part of your SWE process.

agentultra 2y ago
And it's not necessary for every project. It's nice to have when it is though. The cost is coming down. Proof automation is incredible today and rapidly improving. This is the part that does the tedious parts of a proof for you so that you can focus on the theorems that matter. The languages and proof systems themselves are easier than ever to pick up and use which is bringing the skill cost down. I don't think most software projects need a huge, dedicated team of specialists to benefit from formal software verification.