[NovemberWhiskey]

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

[Veserv]

Using existing techniques, the formal specification is almost always multiple times larger than a formally correct implementation. The accompanying proof is then tens to hundreds of times larger than the specification assuming one is even constructible at all (which is basically only true for small programs).

Luckily, a sound proof verification engine is feasible, so you are unlikely to have a "proof error" despite the proof "implementation" being so much larger. But, the fact that the specification is much larger than the implementation means there is more room for specification errors than implementation errors. The reason why you might still want a formal specification even if it is larger is that you can prove it and you can formally reason about the specification, goals, and interactions. It remains to be seen if we can invent a way to consistently make a formal specification simpler than the implementation which would be the holy grail as there would be no downsides.

[pydry]

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]

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]

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.

[NovemberWhiskey]

This is the thing that I'm finding difficulty with - the formal specification isn't an alternative to an informal specification; it should go along with one.

Specification "by example" is, in my experience, almost guaranteed to result in missed cases or unspecified behaviors in uncommon situations.

[pydry]

>This is the thing that I'm finding difficulty with - the formal specification isn't an alternative to an informal specification; it should go along with one.

Why are you finding difficulty with that? Not having formal verification is an alternative to having a formal verification.

There ought to be a cost/benefit analysis applied to the tool - i.e. does the cost of writing and maintaining the formal specification pay for itself in terms of bugs caught. Does it have the potential to create new kinds of bugs? (I would argue yes).

The common belief is that it does bring value for certain types of code (rocket ships, maybe pacemakers? etc.), however very few people actually use it because for most applications a certain level of bugginess is perfectly fine. As a result, very few people actually have experience with it.

>Specification "by example" is, in my experience, almost guaranteed to result in missed cases or unspecified behaviors in uncommon situations.

Specification by example does mean missed cases, yes, but the missed cases will get caught by manual testers involved in the process of writing the examples, programmers while implementing the code or fuzz testing.

The dysfunctions I tend to see aren't edge case scenarios being missed altogether, but:

* Not involving programmers / testers who would spot the edge cases in the process of writing the examples. This is typically an organizational dysfunction.

* The programmer decides themselves what the correct behavior should be during edge cases without consulting the stakeholders.

* The PO/PM/Developers make poor decisions about overall architecture or intended edge case behavior. A large part of good system design involves constraining the number of inputs to a system so that the number of potential scenarios doesn't explode unmanageably.

The question I think formal verification has to answer is - does it actually bring any value if you are already doing all of those things or is it more of a performative ritual to ward off the bug spirits?