6 ms·

This is an excellent blog post. If you believe a proof of correctness produced by a formal verification tool, I have a bridge to sell you. For a proof of corr

This is an excellent blog post. If you believe a proof of correctness produced by a formal verification tool, I have a bridge to sell you. For a proof of correctness, you need to model the environment, and write a specification or a golden model. These are just as prone to bugs as the system you are trying to verify (even assuming the tools are correct). That is not to say formal verification is useless. Developing a proof will force you to formalize your intuitive grasp of the system and its interfaces. Counterexamples produced by the tools will often help to find deep bugs that would be almost impossible to find any other way. And after many iterations of debugging both the system and the proof, you might gain a lot of confidence in the proof and the system. But even after all of that, trusting a formal proof as a guarantee of correctness is insane.

mbid 9y ago
As far as I can tell, the formal proofs themselves were always correct in his example. The problem was that the proved statements were not the ones intended.
ique 9y ago
What you're saying is just "trusting any system is insane", which sure, it might be (depending on the criticalness of said system). But that's not very insightful or informative, how does that drive any sort of decision-making or improvement process? Do you have any suggestion on how to improve the correctness of systems that work better than formal verification?
- edanm 9y ago
  QA testing on various levels, and real-world usage without incident? This is what most software does and it seems to work fine in the real world, in most cases at least.
  - hateduser2 9y ago
    >it seems to work fine in the real world I thought the whole premise of this conversation was that this is a total fabrication?
    - abritinthebay 9y ago
      I don’t believe so - I think it was it isn’t formally showing it is correct. Which is true.
- oldgradstudent 9y ago
  Formal verification techniques can be very useful, especially for finding deep, often insanely complex bugs. The process of developing the proof can produce a lot of insight about the system and expose hidden assumptions that were never considered while designing the system. It is the final proof itself which is the problem. It does not contribute anything except for terminating the debugging process. Because the specification can be just complex as the system, the proof can only provide a false sense of security. A correctness theatre.
  - zzzcpan 9y ago
    This is what many people are missing in their understanding of formal verification. Things that reduce bugs are not proofs, but a different thought process that sort of double checks everything from a different perspective.
  - seanwilson 9y ago
    > Because the specification can be just complex as the system Can you give an example of this? I don't find this true in general at all e.g. writing the specification of a sorting algorithm is much easier than implementing most practical sorting algorithms. > the proof can only provide a false sense of security. A correctness theatre. You could use this argument to say that unit tests, type systems, code review etc. are correctness theatre. All these things prevent mistakes.
    - mafribe 9y ago
      > Can you give an example of this? It's pretty clear that a fully formal specification of a program must be (roughly) as complex as the program itself, for otherwise you could construct an infinitely descending chain of ever simpler specifications which leads to a contradiction. The reason that you found the specification of a sorting algorithm simpler than the sorting algorithm is that you probably have not fully specified the algorithm. Consider the sorting algorithm in C's standard library, which allows the user to specify a comparison function. Now imagine you'd pass something like the following comparison function: def compare (x, y): printf ( "I'm comparing %i with %i\n", x, y ) if ( x < y ) return 1 if ( x == y ) return 0 else return -1 It almost completely exposes the inner workings of sorting. Hence a full spec needs to account for this.
- abritinthebay 9y ago
  Trusting any sufficiently complex system to be correct is insane. It’s virtually impossible to do and be confident at all levels your proof is correct once you move past much more than trivial systems. This is why modern software testing takes a more... I guess you could call it Bayesian... approach. QA, unit testing, integration testing, etc - these are all ways of reducing probabilities of incorrectness. Never formally prove it of course, but make your confidence higher with each. So suggestions? Proper testing and QA.
  - lmm 9y ago
    > QA, unit testing, integration testing, etc - these are all ways of reducing probabilities of incorrectness. Never formally prove it of course, but make your confidence higher with each. And formal proofs don't make your confidence higher? IME they're the most efficient tool in the toolbox if you need to get to really low defect rates. (Of course, the sad economic reality is that for most consumer software even a 5% defect rate is perfectly acceptable).
    - zzzcpan 9y ago
      It's not that simple. Defects don't necessarily have to cause problems, depending on how you design your software (think OTP-style architecture). And avoiding problems is in fact what you always need, not low defect rates. It's just so happens that sometimes you can only achieve decent reliability by pursuing very low defect rates. But for a lot of software it cannot economically beat other approaches.
    - abritinthebay 9y ago
      Given a formal proof of a complex system that doesn’t contain any assumptions or mis-modeling is - practically speaking - unachievable... ... then in comparison the time is better spent on something that will produce demonstratable results, even if imperfectly applied. And that is QA & testing.
      - lmm 9y ago
        > the time is better spent on something that will produce demonstratable results, even if imperfectly applied. How is formal proof not such a thing?
ghettoimp 9y ago
"For a proof of correctness, you need to model the environment, and write a specification or a golden model. These are just as prone to bugs as the system you are trying to verify (even assuming the tools are correct)." I disagree with the idea that a spec is as buggy as the implementation. Some examples. In hardware verification, a spec for a floating-point operation is typically a page or two long. The corresponding RTL implementations can be tens of thousands of lines, with many additional concerns (pipelining, clock gating, ...) that don't show up in the spec, and where the operation itself is fused together with dozens of other operations. The difference in complexity is striking. In simple software cases, say a sorting function, the spec can be as straightforward as "the answer is ordered and has the same elements as the input array." This same spec can be used with any number of implementations, including things like Timsort where there are multiple modes and optimizations that are interacting with one another. The spec says nothing about runs, galloping, etc., which the implementation uses. For more complex software, the spec can of course become complex. Even so, there are examples, e.g., the Jitawa Lisp runtime (https://www.cl.cam.ac.uk/~mom22/jitawa/ https://www.cl.cam.ac.uk/~mom22/jitawa/), where the spec is a relatively straightforward description of a programming language that is much, much simpler than the implementation. For instance, the spec here does not mention things like garbage collection and just-in-time compilation, which are fairly complex features of the implementation. Anyway, trusting a formal proof seems, to me, certainly no less sane than trusting a system without such a proof.
- crdoconnor 9y ago
  >I disagree with the idea that a spec is as buggy as the implementation. Some examples. It isn't necessarily as buggy as implementation, but I've worked on plenty of (non-formally verified) projects where the majority of bugs were spec bugs. If you're diligent about following the UNIX philosophy of assembling small self-contained, tightly specified (and test driven) components, this is pretty normal I think. Building the wrong thing is often the biggest problem. The one time I did do formal verification (at uni) that was certainly the case too, though that may partly have been because the language was an overcomplicated pile of crap (Z). One of my co-workers also told me a story about a formally verified program being translated into python and having a couple of bugs picked up on the way. I'm pretty credulous of this.
protonfish 9y ago
Fred Brooks said it years ago: "Even perfect program verification can only establish that a program meets its specification. … Much of the essence of building a program is in fact the debugging of the specification."

mbid 9y ago

As far as I can tell, the formal proofs themselves were always correct in his example. The problem was that the proved statements were not the ones intended.

ique 9y ago

What you're saying is just "trusting any system is insane", which sure, it might be (depending on the criticalness of said system). But that's not very insightful or informative, how does that drive any sort of decision-making or improvement process? Do you have any suggestion on how to improve the correctness of systems that work better than formal verification?

edanm 9y ago
QA testing on various levels, and real-world usage without incident? This is what most software does and it seems to work fine in the real world, in most cases at least.
- hateduser2 9y ago
  >it seems to work fine in the real world I thought the whole premise of this conversation was that this is a total fabrication?
  - abritinthebay 9y ago
    I don’t believe so - I think it was it isn’t formally showing it is correct. Which is true.
oldgradstudent 9y ago
Formal verification techniques can be very useful, especially for finding deep, often insanely complex bugs. The process of developing the proof can produce a lot of insight about the system and expose hidden assumptions that were never considered while designing the system. It is the final proof itself which is the problem. It does not contribute anything except for terminating the debugging process. Because the specification can be just complex as the system, the proof can only provide a false sense of security. A correctness theatre.
- zzzcpan 9y ago
  This is what many people are missing in their understanding of formal verification. Things that reduce bugs are not proofs, but a different thought process that sort of double checks everything from a different perspective.
- seanwilson 9y ago
  > Because the specification can be just complex as the system Can you give an example of this? I don't find this true in general at all e.g. writing the specification of a sorting algorithm is much easier than implementing most practical sorting algorithms. > the proof can only provide a false sense of security. A correctness theatre. You could use this argument to say that unit tests, type systems, code review etc. are correctness theatre. All these things prevent mistakes.
  - mafribe 9y ago
    > Can you give an example of this? It's pretty clear that a fully formal specification of a program must be (roughly) as complex as the program itself, for otherwise you could construct an infinitely descending chain of ever simpler specifications which leads to a contradiction. The reason that you found the specification of a sorting algorithm simpler than the sorting algorithm is that you probably have not fully specified the algorithm. Consider the sorting algorithm in C's standard library, which allows the user to specify a comparison function. Now imagine you'd pass something like the following comparison function: def compare (x, y): printf ( "I'm comparing %i with %i\n", x, y ) if ( x < y ) return 1 if ( x == y ) return 0 else return -1 It almost completely exposes the inner workings of sorting. Hence a full spec needs to account for this.
abritinthebay 9y ago
Trusting any sufficiently complex system to be correct is insane. It’s virtually impossible to do and be confident at all levels your proof is correct once you move past much more than trivial systems. This is why modern software testing takes a more... I guess you could call it Bayesian... approach. QA, unit testing, integration testing, etc - these are all ways of reducing probabilities of incorrectness. Never formally prove it of course, but make your confidence higher with each. So suggestions? Proper testing and QA.
- lmm 9y ago
  > QA, unit testing, integration testing, etc - these are all ways of reducing probabilities of incorrectness. Never formally prove it of course, but make your confidence higher with each. And formal proofs don't make your confidence higher? IME they're the most efficient tool in the toolbox if you need to get to really low defect rates. (Of course, the sad economic reality is that for most consumer software even a 5% defect rate is perfectly acceptable).
  - zzzcpan 9y ago
    It's not that simple. Defects don't necessarily have to cause problems, depending on how you design your software (think OTP-style architecture). And avoiding problems is in fact what you always need, not low defect rates. It's just so happens that sometimes you can only achieve decent reliability by pursuing very low defect rates. But for a lot of software it cannot economically beat other approaches.
  - abritinthebay 9y ago
    Given a formal proof of a complex system that doesn’t contain any assumptions or mis-modeling is - practically speaking - unachievable... ... then in comparison the time is better spent on something that will produce demonstratable results, even if imperfectly applied. And that is QA & testing.
    - lmm 9y ago
      > the time is better spent on something that will produce demonstratable results, even if imperfectly applied. How is formal proof not such a thing?

ghettoimp 9y ago

"For a proof of correctness, you need to model the environment, and write a specification or a golden model. These are just as prone to bugs as the system you are trying to verify (even assuming the tools are correct)." I disagree with the idea that a spec is as buggy as the implementation. Some examples. In hardware verification, a spec for a floating-point operation is typically a page or two long. The corresponding RTL implementations can be tens of thousands of lines, with many additional concerns (pipelining, clock gating, ...) that don't show up in the spec, and where the operation itself is fused together with dozens of other operations. The difference in complexity is striking. In simple software cases, say a sorting function, the spec can be as straightforward as "the answer is ordered and has the same elements as the input array." This same spec can be used with any number of implementations, including things like Timsort where there are multiple modes and optimizations that are interacting with one another. The spec says nothing about runs, galloping, etc., which the implementation uses. For more complex software, the spec can of course become complex. Even so, there are examples, e.g., the Jitawa Lisp runtime (https://www.cl.cam.ac.uk/~mom22/jitawa/ https://www.cl.cam.ac.uk/~mom22/jitawa/), where the spec is a relatively straightforward description of a programming language that is much, much simpler than the implementation. For instance, the spec here does not mention things like garbage collection and just-in-time compilation, which are fairly complex features of the implementation. Anyway, trusting a formal proof seems, to me, certainly no less sane than trusting a system without such a proof.

crdoconnor 9y ago
>I disagree with the idea that a spec is as buggy as the implementation. Some examples. It isn't necessarily as buggy as implementation, but I've worked on plenty of (non-formally verified) projects where the majority of bugs were spec bugs. If you're diligent about following the UNIX philosophy of assembling small self-contained, tightly specified (and test driven) components, this is pretty normal I think. Building the wrong thing is often the biggest problem. The one time I did do formal verification (at uni) that was certainly the case too, though that may partly have been because the language was an overcomplicated pile of crap (Z). One of my co-workers also told me a story about a formally verified program being translated into python and having a couple of bugs picked up on the way. I'm pretty credulous of this.

protonfish 9y ago

Fred Brooks said it years ago: "Even perfect program verification can only establish that a program meets its specification. … Much of the essence of building a program is in fact the debugging of the specification."