[pydry]

My biggest issue with formal verification after doing it a couple of times was how absurdly complex the specification needed to be for it to work.

If the spec is 5x more complicated than the code would be then I'm not sure I see much of a point coz you're just creating different spaces for bugs to hide in.

[mbrock]

The aim is to have a spec that is much LESS complex than the code, written at a higher level, abstracting away details. If the spec is 5x more complex than the code then indeed there’s no point.

[qznc]

Here is a counter argument: http://www.pathsensitive.com/2018/10/book-review-philosophy-...

My summary would be: The spec must cover all possible implementations so it is usually larger than the most simple one.

An example from there:

> The authors of SibylFS tried to write down an exact description of the `open` interface. Their annotated version of the POSIX standard is over 3000 words. Not counting basic machinery, it took them over 200 lines to write down the properties of `open` in higher-order logic, and another 70 to give the interactions between open and close.

> For comparison, while it’s difficult to do the accounting for the size of a feature, their model implementation is a mere 40 lines.

[jacobr1]

How much of that is open/close being a poor abstraction, or overloading a bunch of semi-related functionality vs a more generalizable consideration systems designed with verification in mind.

[szatkus]

Do you have any rule of thumb for that? Like, I have 1000 LOCs, how many lines of spec I could except for that code?