[toast0]

The first part of formal verification is getting a formal specification. I don't know about most developers, but I rarely get a written specification for anything I work on, and when I do, it's no where near what would be needed to turn it into a formal specification.

Anyway, the specification is subject to change at the whim of a hat, so putting a lot of effort into verifying it is foolish.

I do see value in formal verification of IPC/threading communication primitives (locks, semaphores, queues, whatevs), but then formal verification usually require assumptions for hardware behavior and those aren't always correct, so. But I've never used formal methods outside exposure in an undergrad survey class, so I dunno.

[derdi]

Nitpick: You don't necessarily need any specification at all in order to reap benefits. Formal verification languages come with a lot of conditions that your program must fulfill in order to be accepted: Every loop terminates, every object you want to read/write is non-null, every list or array access is in bounds, etc.

For example, if you load an arbitrary C program into Frama-C, you'll have tons of properties to prove before you can even think of adding your own specification. The promises you get is that the program will always terminate and will never invoke undefined behavior. These properties are extremely useful, and these requirements are unlikely to change! And yes, C is... special. But pretty much any language has lists or arrays, nullable/option types, and unbounded loops. "No crashes/panics/uncaught exceptions" should be worth it.

And then, even absent a specification, you can start modeling invariants of the system anyway. This list is always sorted, this number is always strictly positive, this data structure never contains duplicate entries, etc. Anything that today would be a comment saying: "Important! The caller must ensure that..." This can help you gain confidence in your system. And if some day a requirement comes along that really requires you to violate one of these invariants, well, you can just remove it, the same way you would remove a test that no longer reflects something that should hold.

[dfabulich]

> "No crashes/panics/uncaught exceptions" should be worth it.

Surprisingly, no. Property-based testing and formal validation make it easy to spend tons of time and money "preventing" bugs that would never have occurred in production, especially uncaught exceptions.

There is code where strong guarantees can be worth it, (databases, platforms/operating systems, parsers accepting hostile input) but it's not most application-level code, and certainly not most e-commerce CRUD apps.

Remember, we're here to make users' lives better, not to write correct code for its own sake.

[derdi]

One problem with the "won't happen in production" argument is that humans are demonstrably bad at predicting "won't happen in production" situations.

[toast0]

> The promises you get is that the program will always terminate

I don't want my programs to terminate though.

[derdi]

Oh no, you have just proved formal verification useless! Or, if you have an outer event loop that should potentially run forever, you mark only that one loop accordingly (details depend on the system).

[weitendorf]

Nothing stops you from writing a formal spec for an implementation or the technical parts of a problem that the product / upstream requirements don't explicitly demand. In fact I would say this is a large part of what software engineering fundamentally is; the reason specs are written in a certain way is because they model a problem domain and encode fundamental (or incidental, which could still be very well-reasoned, eg due to backwards compatibility, limitations of dependencies, or practical constraints) properties that are unlikely to change. Once you've actually written software that other systems/components are depending on, you've in practice created a spec. And it's a false dichotomy to think that just because there is no formalized spec for something before it's implemented at all, that this means that once the domain is better understood or stabilizied, you cannot use formal verification on the de-facto spec that has been arrived at/de-jure rules and structure that are prescribed but not yet formalized.

Even when you are writing something for the first time, like a parser for a certain kind of data format, you often can greatly accelerate your production-safety/security maturity by formalizing your spec enough to be fuzzed and to use existing parsing tooling that avoids the footguns most developers will introduce writing their own parsers from scratch. This is IMO the most common situation in which formal verification becomes very useful; even if the data format is purely an implementaton detail, any time parsing untrusted/user-provided input is involved, it would be much more foolish to try to just throw together some random string processing functions than to use something like flex/bison, an existing serialization format/protocol, or a metaparser (which may themselves be formally verified).

[AnimalMuppet]

At my last job, I got a formal specification for one project. But the implementation happened in parallel for time reasons, so by the time the spec was frozen, 90% of the code was written.

[aezart]

What we get typically is a second or third-hand summary of an analysis someone else did about how the current version works, with no indication of what stuff has to stay as-is in our replacement and what stuff can be improved.