[carlmr]

I think the biggest issue with formal verification, is that you need to rewrite the important parts of your code in (for example) TLA+. If it's integrated into the language, like ADA Spark, you don't need to learn so much additional syntax or rewrite parts of your codebase in a language you rarely use (given that you already work in ADA).

[ahelwer]

Well, you can't rewrite anything in TLA+. It's a formal specification language, not verification language. So you usually use it to catch spec- or algorithm-level logic & concurrency bugs then manually write the code to correspond to your TLA+ spec. People get really hung up on this last step, but I can tell you as a professional programmer that implementing code to follow a TLA+ spec is extremely easy - all the intellectual heavy lifting has already been done! - and avoids the extremely costly effort required to fully formally verify computer code. It's a great cost/benefit ratio.

[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?