4 ms·

My experience with formal specifications was that our specification ended up being more complex than the code itself. This is a tricky problem, because your sp

by pydry 3y ago

My experience with formal specifications was that our specification ended up being more complex than the code itself. This is a tricky problem, because your specifications can and usually does have bugs. I once measured this on a project I worked on and found that it accounted for up to ~60% of all incoming bugs - that is, 60% of bugs were due to misunderstandings or miscommunications involving a spec of some kind. The added complexity of formal verification languages creates an opening for specification bugs to creep in. The net effect was that we might have had 0 code bugs via this automatic proving system but the number of bugs in the specification actually went up. I'm been deeply cynical about formal verification ever since. I'm not even of the opinion that it's "maybe not good for us, but good for building code for rocket ships". I think it might be actually bad at that too. I'm bullish on more sophisticated type systems and more sophisticated testing, but not formal verification.

AnimalMuppet 3y ago
First, did you (or anyone) write up the results from your measurement? That sounds like empirical data on a subject where I have never heard of their being data, so it would be really useful to capture it. Second: > The net effect was that we might have had 0 code bugs via this automatic proving system but the number of bugs in the specification actually went up. Are you saying that this is part of what you measured? Or are you merely saying that this is hypothetically a way things could work out?
- NovemberWhiskey 3y ago
  >That sounds like empirical data on a subject where I have never heard of their being data c.f. https://userweb.cs.txstate.edu/~rp31/papers/KingHammondChapmanPryor.pdf https://userweb.cs.txstate.edu/~rp31/papers/KingHammondChapm...
  - pfdietz 3y ago
    Formal proof of correctness vs. manually created tests. The comparison should be formal proof of correctness vs. fuzzing using the formal specification as a source of properties to be tested.
    - NovemberWhiskey 3y ago
      Fuzzing is a statistical technique that isn't ever going to give you a reassurance that a problem doesn't exist. It's great at giving you counterexamples, so fuzzing is great for discovering vulnerabilities, but unless you're fuzzing your program's entire state-space (which is absolutely impossible for even relatively small programs) then you're not comparing like with like.
      - pfdietz 3y ago
        So? The paper compared formal techniques vs. testing. Why is that suddenly not appropriate if the testing is fuzzing?
      - pydry 3y ago
        >Fuzzing is a statistical technique that isn't ever going to give you a reassurance that a problem doesn't exist. Formal verification doesn't prove that bugs don't exist either, thanks to the aforementioned "bugs in the spec" scenario.
- pydry 3y ago
  >Are you saying that this is part of what you measured? Or are you merely saying that this is hypothetically a way things could work out? I'm saying that, anecdotally, when I tried it I had more bugs thanks to formal verification because bugs crept into the spec. It was very hard to tell that those bugs were present because the spec was very, very complicated. I'm not denying that it can catch bugs at all, just that a successful "proof" didn't mean a lack of bugs and that I personally found it to be a relatively inefficient method of catching bugs (or demonstrating their nonexistence).
NovemberWhiskey 3y ago
>This is a tricky problem, because your specifications can and usually does have bugs. I once measured this on a project I worked on and found that it accounted for up to ~60% of all incoming bugs - that is, 60% of bugs were due to misunderstandings or miscommunications involving a spec of some kind. Well, OK, but the reason you have "bugs" in your specifications is usually that the English-language (or whatever you have) informal requirements documentation is imprecise, ambiguous or contradictory. At least with a formal specification, you shouldn't have that problem.
- pydry 3y ago
  There are *lots* of potential reasons for specification bugs. Informally delivered requirements is just one of them and I'm not sure it is even the most common. Formal specification languages are more likely to have specification bugs despite being precise and unambiguous for the same reason programming languages have bugs despite being precise and unambiguous: they are complicated and extremely expressive languages which means a larger scope for mistakes, misunderstandings and accidental misinterpretation. Were formal specification languages straightforward and simple the scope for misunderstanding and misinterpretation would decline, but so would the power to "prove" the code is free of bugs.
  - NovemberWhiskey 3y ago
    More likely than what? Informal specifications? My primary experience with formal specifications is as part of a literate specification, where you would have a rigorous English-language explanation interspersed with the formal specification (e.g. Z schemata). A reader can look at the formal specification and the English and decide whether they think they mean the same thing; experience suggests that most engineers or people with STEM-type backgrounds need no more than a few days of training to be able to read Z (even if they can't write it). The document as a whole can be type-checked, which is a lightweight way to check for the most egregious kinds of errors.
    - pydry 3y ago
      More likely than semi formal. The normal way I get specs is not via a drunk phone call (thank god) but via jira tickets that have been discussed and list concrete examples. I think this is pretty normal for many people. I received training in Z and I balk at the idea of reading it. Though you dont seem to believe it, I can well believe that the gap between the English language spec and the formal spec is easily desynchronized and infested with bugs.
someplaceguy 3y ago
> your specifications can and usually does have bugs One cool thing about formal verification is that you can not only prove things about your code, but you can prove things about the specification itself (with some approaches, at least). This includes proving arbitrary properties, proving the presence of bugs, proving the absence of bugs and in some cases, even proving full correctness of the specification. > I'm bullish on more sophisticated type systems [...] but not formal verification. I don't know what kind of formal verification framework you used that left you with this conclusion, but the more sophisticated is your type system, the closer you are to doing formal verification.
- pydry 3y ago
  Z notation is the framework which left me with this conclusion. It was allegedly named this by its founder because it is "the ultimate" language. I thought it was terrible. I've used plenty of type systems, and they have all provided a means to annotate the code and then prove certain properties about the code, but I have never in my life seen a type system which let me define a whole specification as formal verification does. I have also seen type systems go waaaay overboard. They ended up inhibiting development velocity because they were so intent on forcing the programmer prove of the code properties that actually didn't need to be proven. In general, I think type systems that try to strongly limit the scope of the properties they are trying to prove and apply a cost/benefit trade off to the value of the proven properties and the costs of the annotation work best.

by pydry 3y ago

AnimalMuppet 3y ago

First, did you (or anyone) write up the results from your measurement? That sounds like empirical data on a subject where I have never heard of their being data, so it would be really useful to capture it. Second: > The net effect was that we might have had 0 code bugs via this automatic proving system but the number of bugs in the specification actually went up. Are you saying that this is part of what you measured? Or are you merely saying that this is hypothetically a way things could work out?

NovemberWhiskey 3y ago
>That sounds like empirical data on a subject where I have never heard of their being data c.f. https://userweb.cs.txstate.edu/~rp31/papers/KingHammondChapmanPryor.pdf https://userweb.cs.txstate.edu/~rp31/papers/KingHammondChapm...
- pfdietz 3y ago
  Formal proof of correctness vs. manually created tests. The comparison should be formal proof of correctness vs. fuzzing using the formal specification as a source of properties to be tested.
  - NovemberWhiskey 3y ago
    Fuzzing is a statistical technique that isn't ever going to give you a reassurance that a problem doesn't exist. It's great at giving you counterexamples, so fuzzing is great for discovering vulnerabilities, but unless you're fuzzing your program's entire state-space (which is absolutely impossible for even relatively small programs) then you're not comparing like with like.
    - pfdietz 3y ago
      So? The paper compared formal techniques vs. testing. Why is that suddenly not appropriate if the testing is fuzzing?
    - pydry 3y ago
      >Fuzzing is a statistical technique that isn't ever going to give you a reassurance that a problem doesn't exist. Formal verification doesn't prove that bugs don't exist either, thanks to the aforementioned "bugs in the spec" scenario.
pydry 3y ago
>Are you saying that this is part of what you measured? Or are you merely saying that this is hypothetically a way things could work out? I'm saying that, anecdotally, when I tried it I had more bugs thanks to formal verification because bugs crept into the spec. It was very hard to tell that those bugs were present because the spec was very, very complicated. I'm not denying that it can catch bugs at all, just that a successful "proof" didn't mean a lack of bugs and that I personally found it to be a relatively inefficient method of catching bugs (or demonstrating their nonexistence).

NovemberWhiskey 3y ago

>This is a tricky problem, because your specifications can and usually does have bugs. I once measured this on a project I worked on and found that it accounted for up to ~60% of all incoming bugs - that is, 60% of bugs were due to misunderstandings or miscommunications involving a spec of some kind. Well, OK, but the reason you have "bugs" in your specifications is usually that the English-language (or whatever you have) informal requirements documentation is imprecise, ambiguous or contradictory. At least with a formal specification, you shouldn't have that problem.

pydry 3y ago
There are *lots* of potential reasons for specification bugs. Informally delivered requirements is just one of them and I'm not sure it is even the most common. Formal specification languages are more likely to have specification bugs despite being precise and unambiguous for the same reason programming languages have bugs despite being precise and unambiguous: they are complicated and extremely expressive languages which means a larger scope for mistakes, misunderstandings and accidental misinterpretation. Were formal specification languages straightforward and simple the scope for misunderstanding and misinterpretation would decline, but so would the power to "prove" the code is free of bugs.
- NovemberWhiskey 3y ago
  More likely than what? Informal specifications? My primary experience with formal specifications is as part of a literate specification, where you would have a rigorous English-language explanation interspersed with the formal specification (e.g. Z schemata). A reader can look at the formal specification and the English and decide whether they think they mean the same thing; experience suggests that most engineers or people with STEM-type backgrounds need no more than a few days of training to be able to read Z (even if they can't write it). The document as a whole can be type-checked, which is a lightweight way to check for the most egregious kinds of errors.
  - pydry 3y ago
    More likely than semi formal. The normal way I get specs is not via a drunk phone call (thank god) but via jira tickets that have been discussed and list concrete examples. I think this is pretty normal for many people. I received training in Z and I balk at the idea of reading it. Though you dont seem to believe it, I can well believe that the gap between the English language spec and the formal spec is easily desynchronized and infested with bugs.

someplaceguy 3y ago

> your specifications can and usually does have bugs One cool thing about formal verification is that you can not only prove things about your code, but you can prove things about the specification itself (with some approaches, at least). This includes proving arbitrary properties, proving the presence of bugs, proving the absence of bugs and in some cases, even proving full correctness of the specification. > I'm bullish on more sophisticated type systems [...] but not formal verification. I don't know what kind of formal verification framework you used that left you with this conclusion, but the more sophisticated is your type system, the closer you are to doing formal verification.

pydry 3y ago
Z notation is the framework which left me with this conclusion. It was allegedly named this by its founder because it is "the ultimate" language. I thought it was terrible. I've used plenty of type systems, and they have all provided a means to annotate the code and then prove certain properties about the code, but I have never in my life seen a type system which let me define a whole specification as formal verification does. I have also seen type systems go waaaay overboard. They ended up inhibiting development velocity because they were so intent on forcing the programmer prove of the code properties that actually didn't need to be proven. In general, I think type systems that try to strongly limit the scope of the properties they are trying to prove and apply a cost/benefit trade off to the value of the proven properties and the costs of the annotation work best.