4 ms·

> 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

by 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.

by atrus 2y ago

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.