4 ms·

Proof is how the authors of this paper discovered that OpenJDK's java.utils.Collection.sort() was broken http://envisage-project.eu/wp-content/uploads/2015/02/

Proof is how the authors of this paper discovered that OpenJDK's java.utils.Collection.sort() was broken http://envisage-project.eu/wp-content/uploads/2015/02/sorting.pdf http://envisage-project.eu/wp-content/uploads/2015/02/sortin...

dehrmann 6y ago
I'm not sure if that's a victory or a loss for formal proofs. Sure, it found the bug, but for a language that popular, it wasn't a very meaningful bug, and sorting algorithms is one of the easier things to analyze.
- ookdatnog 6y ago
  For algorithms without provided proof, we can only estimate their correctness based on how battle-tested they are. If an algorithm has been run many times and it has been correct every one of those times, then we feel somewhat confident that we got it right. Over time, we'll find weird edge cases where it doesn't work, and fix them. Few algorithms are as battle-tested as the sorting algorithm from the Java standard library. I can't even estimate how many calls are made to this function every day. The fact that we can still find bugs in it, no matter how obscure, suggests to me that we simply can't write correct nontrivial software without proof. The victory isn't in showing that this specific algorithm is incorrect in some fairly obscure way. It's in the fact that even software that's this battle-tested is still not fully reliable.
  - dehrmann 6y ago
    > even software that's this battle-tested is still not fully reliable But does it matter? I also don't understand formal methods well, but wouldn't they also be subject to bugs? It seems like all we can do is make software less unreliable.
    - ookdatnog 6y ago
      > But does it matter? That depends on the application. It probably doesn't most of the time. My point is not that it is always economical to use formal methods, just that I suspect their cost is overestimated compared to the benefit (because most programmers are simply unfamiliar with FM). > I also don't understand formal methods well, but wouldn't they also be subject to bugs? Yes, they are. There are multiple classes of errors FM are vulnerable to. 1. In FM you prove your code correct with respect to a specification. But you can make errors in the specification too. The arguments for FM are: a) the spec is much smaller than the program, so the opportunity for error is lower, and spec errors are more obvious; b) often if your spec is wrong, you'll find out when you try to prove your algorithm; and c) combining testing with FM is very likely to uncover whatever errors are left. 2. If your proof of correctness is not mechanically verified, then you may still have trivial implementation errors like mixing up variables and the like. 3. If it is mechanically verified, then theoretically there's still opportunity for errors. The verifier might contain a bug, the compiler might contain a bug, the hardware you run the algorithm on might contain a bug, cosmic radiation may flip a bit during the verification/compilation process, invalidating the correctness, etc. I can soapbox about the implications of this but I will only do that when prompted to :) So indeed, there is no method that gives you zero probability of failure. But you can get the probability orders of magnitude lower, which may be worth it depending on what you're working on.

dehrmann 6y ago

I'm not sure if that's a victory or a loss for formal proofs. Sure, it found the bug, but for a language that popular, it wasn't a very meaningful bug, and sorting algorithms is one of the easier things to analyze.

ookdatnog 6y ago
For algorithms without provided proof, we can only estimate their correctness based on how battle-tested they are. If an algorithm has been run many times and it has been correct every one of those times, then we feel somewhat confident that we got it right. Over time, we'll find weird edge cases where it doesn't work, and fix them. Few algorithms are as battle-tested as the sorting algorithm from the Java standard library. I can't even estimate how many calls are made to this function every day. The fact that we can still find bugs in it, no matter how obscure, suggests to me that we simply can't write correct nontrivial software without proof. The victory isn't in showing that this specific algorithm is incorrect in some fairly obscure way. It's in the fact that even software that's this battle-tested is still not fully reliable.
- dehrmann 6y ago
  > even software that's this battle-tested is still not fully reliable But does it matter? I also don't understand formal methods well, but wouldn't they also be subject to bugs? It seems like all we can do is make software less unreliable.
  - ookdatnog 6y ago
    > But does it matter? That depends on the application. It probably doesn't most of the time. My point is not that it is always economical to use formal methods, just that I suspect their cost is overestimated compared to the benefit (because most programmers are simply unfamiliar with FM). > I also don't understand formal methods well, but wouldn't they also be subject to bugs? Yes, they are. There are multiple classes of errors FM are vulnerable to. 1. In FM you prove your code correct with respect to a specification. But you can make errors in the specification too. The arguments for FM are: a) the spec is much smaller than the program, so the opportunity for error is lower, and spec errors are more obvious; b) often if your spec is wrong, you'll find out when you try to prove your algorithm; and c) combining testing with FM is very likely to uncover whatever errors are left. 2. If your proof of correctness is not mechanically verified, then you may still have trivial implementation errors like mixing up variables and the like. 3. If it is mechanically verified, then theoretically there's still opportunity for errors. The verifier might contain a bug, the compiler might contain a bug, the hardware you run the algorithm on might contain a bug, cosmic radiation may flip a bit during the verification/compilation process, invalidating the correctness, etc. I can soapbox about the implications of this but I will only do that when prompted to :) So indeed, there is no method that gives you zero probability of failure. But you can get the probability orders of magnitude lower, which may be worth it depending on what you're working on.