3 ms·

> I'm not convinced it is necessarily that challenging, because the proof goes with the code. A program source is already an informal proof of correctness - the

> I'm not convinced it is necessarily that challenging, because the proof goes with the code. A program source is already an informal proof of correctness - the reason we tend to believe our programs are correct is that their code looks like it does the correct thing. Few maintainable programs rely on invariants that appear "magically" out of nowhere; a human reader would believe an invariant held because they could see a code path or state that represented that invariant. Have you done any formal proofs before? You're severely underestimating how difficult and time consuming they are to do even if you do have some intuition about why they are correct. The sel4 microkernel took around 5 years for around 20 experts to verify for example. Verifying a program can result in you having to prove arbitrarily difficult maths theorems so it's similar to saying automating arbitrarily difficult maths theorems should be trivial. > I think for most real-world code, the theorem that the code represents (in a Curry-Howard sense) tends to be trivial. Yes, the theorem/specification statement may be trivial compared to the code but the hard part is coming up with the proof that shows the code matches the specification. You don't get this for free.

lmm 11y ago
> Verifying a program can result in you having to prove arbitrarily difficult maths theorems so it's similar to saying automating arbitrarily difficult maths theorems should be trivial. But you wouldn't write a program that depended on a theorem that wasn't proven, no? I mean often the only mathematically hard parts of a given program are in the libraries it uses - which could ship with their own proofs. > Yes, the theorem/specification statement may be trivial compared to the code but the hard part is coming up with the proof that shows the code matches the specification. You don't get this for free. Doesn't the structure of the code tell you how to structure the proof though? Like, if you've written code that appends to a list by appending a single element and recursing, the way you prove it correct is to prove that it appends a single element and that it recurses correctly. If you've written something that's supposed to be a sorting algorithm and the code rearranges the elements of a list, why is it that you believe this particular rearrangement of the elements is a correct sort? Isn't the answer to that question your proof of correctness?
- pron 11y ago
  > Isn't the answer to that question your proof of correctness? If that were the case then we'd never have bugs :) The number of corner cases can be staggering. So the answer to "why do you believe a sorting algorithm sorts?" is "because I considered a few cases, in the hope that it's enough". Whether or not it actually is enough is the source of all bugs. Just take a look at the state-space visualizations of real but positively tiny programs to understand how complex tiny, useful programs are: https://www3.hhu.de/stups/prob/index.php/State_space_visualization_examples https://www3.hhu.de/stups/prob/index.php/State_space_visuali... Some seem structured enough (those are the toy examples), but some are far from it. Or at this program that is known to never throw an exception, yet proving it is... hard: int foo(int x) { if (x <= 2 || (x & 1) != 0) return 0; for (int i = 2; i < x; i++) if (bar(i) && bar(x - i)) return i; throw new AssertionError(); // unreachable } boolean bar(int x) { for (int i = 2; i < x; i++) for (int s = x; s >= 0; s -= i) if (s == 0) return false; return true; } Does this seem like an arbitrarily difficult math theorem (because it is)? See those two lines in the middle of `bar` where the result depends on the depth of the recursion (or loop)? That's what makes the proof incredibly hard, and it is very common in real world programs. Does the structure of the code suggest a proof? Writing this program in Idris and proving that the type of `foo` is `Int` rather than `Maybe Int` is equivalent to proving Goldbach's conjecture. True, most functions don't look like this, but in pretty much every serious project I've seen, there were at least a couple of instances of code that is even more complicated. Now, the real question is where do the expensive bugs lie. In code that's hard to prove or in code that's easy to prove (or equally in both)? That is a question that is certainly worth investigating. But wherever the expensive bugs lie, it's likely not in implementations of list append...
  - lmm 11y ago
    > See those two lines in the middle of `bar` where the result depends on the depth of the recursion (or loop)? That's what makes the proof incredibly hard, and it is very common in real world programs Not my experience, but shrug. > Does the structure of the code suggest a proof? No - but it does look like bad code. > True, most functions don't look like this, but in pretty much every serious project I've seen, there were at least a couple of instances of code that is even more complicated. I've seen code that looks like that, but it's always been easy enough to clear up. As my career goes on I'm starting to think that almost all real-world code is trivial. > Now, the real question is where do the expensive bugs lie. In code that's hard to prove or in code that's easy to prove (or equally in both)? My experience is that most production bugs are stupidly obvious things. And that possibly all bugs are either stupid "why doesn't the compiler catch that" cases, or code that is bad (unreadable) on its face. Possibly that's a tautology. > But wherever the expensive bugs lie, it's likely not in implementations of list append... You say that, but verification of JDK sorting uncovered a real bug.

lmm 11y ago

> Verifying a program can result in you having to prove arbitrarily difficult maths theorems so it's similar to saying automating arbitrarily difficult maths theorems should be trivial. But you wouldn't write a program that depended on a theorem that wasn't proven, no? I mean often the only mathematically hard parts of a given program are in the libraries it uses - which could ship with their own proofs. > Yes, the theorem/specification statement may be trivial compared to the code but the hard part is coming up with the proof that shows the code matches the specification. You don't get this for free. Doesn't the structure of the code tell you how to structure the proof though? Like, if you've written code that appends to a list by appending a single element and recursing, the way you prove it correct is to prove that it appends a single element and that it recurses correctly. If you've written something that's supposed to be a sorting algorithm and the code rearranges the elements of a list, why is it that you believe this particular rearrangement of the elements is a correct sort? Isn't the answer to that question your proof of correctness?

pron 11y ago
> Isn't the answer to that question your proof of correctness? If that were the case then we'd never have bugs :) The number of corner cases can be staggering. So the answer to "why do you believe a sorting algorithm sorts?" is "because I considered a few cases, in the hope that it's enough". Whether or not it actually is enough is the source of all bugs. Just take a look at the state-space visualizations of real but positively tiny programs to understand how complex tiny, useful programs are: https://www3.hhu.de/stups/prob/index.php/State_space_visualization_examples https://www3.hhu.de/stups/prob/index.php/State_space_visuali... Some seem structured enough (those are the toy examples), but some are far from it. Or at this program that is known to never throw an exception, yet proving it is... hard: int foo(int x) { if (x <= 2 || (x & 1) != 0) return 0; for (int i = 2; i < x; i++) if (bar(i) && bar(x - i)) return i; throw new AssertionError(); // unreachable } boolean bar(int x) { for (int i = 2; i < x; i++) for (int s = x; s >= 0; s -= i) if (s == 0) return false; return true; } Does this seem like an arbitrarily difficult math theorem (because it is)? See those two lines in the middle of `bar` where the result depends on the depth of the recursion (or loop)? That's what makes the proof incredibly hard, and it is very common in real world programs. Does the structure of the code suggest a proof? Writing this program in Idris and proving that the type of `foo` is `Int` rather than `Maybe Int` is equivalent to proving Goldbach's conjecture. True, most functions don't look like this, but in pretty much every serious project I've seen, there were at least a couple of instances of code that is even more complicated. Now, the real question is where do the expensive bugs lie. In code that's hard to prove or in code that's easy to prove (or equally in both)? That is a question that is certainly worth investigating. But wherever the expensive bugs lie, it's likely not in implementations of list append...
- lmm 11y ago
  > See those two lines in the middle of `bar` where the result depends on the depth of the recursion (or loop)? That's what makes the proof incredibly hard, and it is very common in real world programs Not my experience, but shrug. > Does the structure of the code suggest a proof? No - but it does look like bad code. > True, most functions don't look like this, but in pretty much every serious project I've seen, there were at least a couple of instances of code that is even more complicated. I've seen code that looks like that, but it's always been easy enough to clear up. As my career goes on I'm starting to think that almost all real-world code is trivial. > Now, the real question is where do the expensive bugs lie. In code that's hard to prove or in code that's easy to prove (or equally in both)? My experience is that most production bugs are stupidly obvious things. And that possibly all bugs are either stupid "why doesn't the compiler catch that" cases, or code that is bad (unreadable) on its face. Possibly that's a tautology. > But wherever the expensive bugs lie, it's likely not in implementations of list append... You say that, but verification of JDK sorting uncovered a real bug.