To me, "this returns sorted lists" illustrates the crux.

You may know exactly what you want, and you may have a reasonably fast and cheap way to verify your code against a formal specification. But the formal specification needs to come from somewhere and for any non-trivial program its complexity is going to be in the same order of magnitude as the code implementing it. So we are back to writing "code" (which is what a formal specification is) that needs to be checked against what we actually want. And that "code" needs .. a test? Hard thinking? A formal verification itself?

Don't believe me that this is hard? Back to "this returns sorted lists". The promise of formal verification is that whatever implementation I throw at the verifier, as long as it passes the check, I'm happy (assuming that I can also encode things like running time and resource use). Now imagine a program that always returns the empty list. It satisfies "this returns sorted lists" trivially but is not at all what we want. The formal spec has a bug. Such issues can be subtle in larger projects and no amount of model checking or SMT solvers can guard you against a bug in that "code".

Don't get me wrong, it can be incredibly useful. But it's not the silver bullet that some proponents make it out to be. It's another tool next to testing, not instead of it. (The whole "testing can only prove the existence of bugs, not their absence, that's why we should use formal verification instead" is just misguided at best and propaganda at worst.)

I think every formal methods phd student who's interested in adoption of their techniques/tools has a short bout of doubt/depression upon realizing just how large of a surface area for bugs lives in a sufficiently useful specification.

This is deeply related to the conceptual error a lot of executives are currently making around automation in/of their software engineering orgs.

It has always been true that learning some formal methods probably makes you a better programmer in certain ways, even if you never use them. I think it's increasingly also true that learning some formal methods probably makes you a better manager of people/processes that product software.

While there is certainly quite a bit of truth to what you say, I have a few counter arguments:

> same order of magnitude as the code implementing it

I believe mathematically formulating what an algorithm should do is very often orders of magnitue simpler than implementing it. As we know from the halting problem, it is easy to specify what the algorithm should do, but it is provably impossible to implement such an algorithm, so there the ratio of complexity is infinite ;)

Also, the huge advantage of a specification is that it is much more compositional than actual code. As the article states, one can just specify (and verify) that the code never crashes totally independent from what the code otherwise should be doing. So one can easily look at each part of the specification and understand why it is a desirable property piece by piece, in much larger isolation than the monolithic totality of the code.

Even more, with a formal specification one can (and probably should, when it gets too compilcated) verify by proof that the spec is internally consistent, i.e. that no part contradicts the requirements of another.

I was attending a conference back in, oh 2017 perhaps, where a few people from Microsoft were discussing their experience adopting TLA+ and somebody made the comment that they found that creating a spec was an exercise that could only meaningfully be done by the engineer (or perhaps team) writing the code. You wouldn’t, say, have an external TLA+ expert write the spec for you, but instead you would use the process of authoring the spec to ultimately learn more about your own design. And of course, perhaps avoid edge case bugs before they are written. Say what you want about Microsoft, but their observation does have a rather large sample size, and it sounded like formal methods was considered more impactful during software design rather than as software verification.

I have a deeper problem. When I'm calling sort() it is useful that it returns a sorted list. However my program rarely has sorted lists of any sort in any requirement. My requirements are around the features my users care about. Sure the list of employees that I need to display needs to be sorted (sometimes by hire date, sometimes by title, sometimes by name - and often combinations of the above), but there are a lot of things I'm doing with that list that are not sorting.

I mean, just for this particular example, you could certainly also add a check that the sorted list is the same length as the input list.

That said, your broader point is more or less correct. I think the advantage of something like TLA+ is that the specs can generally be more abstract and as such the checks can be more exhaustive than you would likely get with regular "code".

With concurrent code, in particular, it can be difficult to know if your algorithm is correct, especially without the confounding variables that you get with a "real" programming language. Is my program broken because of some memory allocation quirk? Is it broken because of some peculiarity with how pthreads are dispatched? Or is my design wrong? Being able to work at an abstract level at least can check the last part.

Of course, though, you are correct that formal methods aren't silver bullets.

I've been using TLA with claude code at work and it roughly takes twice as long, but it's already _fast_ to get claude to produce code and this prevents a lot of rework.

> The promise of formal verification

The promise of formal verification (and testing) is essentially the same promise as double-entry accounting. It assumes that if you do the same thing twice that it is unlikely you will screw it up in the exact same way twice. When there is disagreement it tells you that something went wrong, but you still need to look at both sides to determine which one is wrong. There is no such thing as a panacea, of course.

> It's another tool next to testing, not instead of it.

Theoretically it is instead of. They both are trying to solve the exact same problem. The real world with real constraints isn't so neat and tidy, so they don't end up perfectly overlapping.