[teiferer]

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

[fultonn]

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.

[shermantanktop]

Execs will often hand-wave away complexity as being irrelevant detail. And sometimes it is - especially if an urgent directional decision is needed.

The key skill - which is rare - is knowing exactly how much analysis to do.

Formal methods are appealing because they suggest that full analysis is possible. But formally proved programs can still have bugs!

[fultonn]

I think you probably got this, but spelling it out anyways for future readers.

The conceptual gap I'm referring to here has nothing to do with formal methods per se. It's just an analogous problem with the quanta of information required to state the spec vs the quanta of information required to state the implementation.

Namely: once your problem has enough of a certain type of essential complexity, there's not a huge delta between "a sufficiently specific description of the problem" and "the source code that solves the problem". The complexity of a sufficiently specific prompt approaches the complexity of the actual solution. At that point, the former does not have the purported benefit and the latter has a lot of huge benefits (determinism, modularity, etc).

When one is operating in that regime of problems, proposing that one can substantially automate the software engineering function has a real "I am not able rightly to apprehend the kind of confusion of ideas that could provoke such a question" feel to it.

[teiferer]

Well put, thank you.

One thing I should say though is that the spec has the luxury of being free of some constraints that the implementation has. For example, the functional spec of a sorting function could describe the shape of the required output without having to say how to arrive there. Or in more complicated cases it could afford an exponential simple algorithm to say that the actual implementation must be functionally equivalent. That may make it simpler because it's free of having to run in linear or whatever time complexity.

[fultonn]

Yes, it's probably the most important trick in formal methods. Often surprisingly difficult to make it actually work, but when it does you can end up with a powerful tool.

In a past life I spent a lot of time on that sort of thing for control systems and RL. Spec says what not to do, reward says what to do, implementation can be arbitrarily complex wrt the spec.

There are many opportunities for an analogous move in LLM-assisted software engineering.

[shermantanktop]

Right, it's a map with a scale of 1:1.

A map with a scale of 100:1 is perfectly useful for navigation. It's just no good for specifying the terrain you want to build with any precision.

[win311fwg]

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

[kilobaud]

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.

[phafu]

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.

[ip26]

It's a complementary tool that replaces certain difficult types of testing. Viewed this way, you can focus writing formal specification for things which are easy & clear to formally specify. "this returns sorted lists" is, for example, a simple property. Other examples might be the O(n) performance of your algorithm. Meanwhile, "every input can be found in the output" might feel too painful to write, so you might compromise on "the output has the same number of elements as the input". This leaves plenty of space for classical testing, while unburdening classical testing from worrying about select classes of bugs.

One other valuable part of formal methods is forcing the author to make claims about their program, and then poking holes in those claims. This process helps the author understand their own code better, and after a process of iteration developing the formal properties that are actually true, you now have a strictly-true external interface specification for the program. This is obviously most-valuable for only certain classes of code, such as libraries or services.

[empath75]

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.

[baq]

Been having LLMs make TLA+ models since the winter and it does work wonders for complex stuff, I guess for the same reason it works for humans: the process of building the model helps when designing the code even if the model is thrown away later (I keep mine though)

[bluGill]

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.

[teiferer]

In which way is that a "deeper" problem? What you are doing with that data can also be expressed as a formal spec.

Sorting is just used as an example everywhere because everybody knows exactly what we are talking about without having to explain a lot, it has a somewhat easy solution space and everybody has implemented some form at some point, likely in school, for the same reasons . Of course real world software is more complex that that but that's not the point.

[pocksuppet]

Actually, sorting a list is an example of something really easy to specify: for each pair of two elements, the one that comes first is less than or equal to the one that comes second.

[Jtsummers]

> for each pair of two elements, the one that comes first is less than or equal to the one that comes second.

That's the property that the result is sorted, but not that you've performed the desired task of sorting a particular list. You also need a post-condition saying that each item in the original is in the destination and with the same number of occurrences.

If you just require that the result be sorted, then this is a valid sort:

  def sorted(ls):
    return []

If you require that it be sorted and contain the same items (but don't check the count), then this is technically sufficient (I've abstracted the actual sort operation out):

  def sorted(ls):
    ls = list(set(ls)) # removes duplicates
    # perform sort
    return result

If you get to the right post-condition, it has to have the same items and the same count and be sorted, then it will satisfy this test:

  def sorted_postcondition(original, result):
    return all(x <= y for x, y in pairwise(result)) and Counter(original) == Counter(result) # Counter is being used as a multiset

[touisteur]

Yes it gets hard really fast. We had a fun (if tongue-in-cheek) exploration of this (proving a sort implementation) with Yannick Moy of SPARK fame some time ago https://www.adacore.com/blog/i-cant-believe-that-i-can-prove...

I only regret not writing the obvious-but-buggy code that "forgot" or added some values and still passed proof...

[pocksuppet]

Aaaaaand now it's a good demonstration of why specifications are not as easy as they seem.

[Jtsummers]

It mostly just takes practice. A good way to get into it is with property-based testing. It's less formal, but you end up expressing many of the same things (you're at least expressing the post-conditions, if not the rest of the things needed for a proof). With practice, you'll start to understand your systems better, and things like what I wrote up will come to you more easily when analyzing and designing them.

To move towards formal proofs of code, I like Leino's Program Proofs (uses Dafny), one of the more approachable tutorials on the subject.

[teiferer]

> It mostly just takes practice

If practice is enough to get a formal system to be correct then why are we doing all this in the first place? Just write correct software! Oh, you can make mistakes? Exaclty! Just like when writing the spec.

[Jtsummers]

> If practice is enough

If that is what you got from my comment, then you did not read my comment.

[tombert]

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.

[mattkrause]

I think you'd want to specify that every element in the original list is present in the sorted list (and in the same number, in case of ties).

And of course, that raises the issue of what do you want to do about ties....

[teiferer]

> 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

Thanks for this fantastic extension of my example, because that is still incomplete Input [2, 1, 3] and output [1, 1, 1]. Matches your revised spec, still wrong.

If multiple smart software engineers get this simple problem wrong, then how many corpses are burried in the average formal spec? Unless it has gone through rigorous review and testing. Which could have been done to the code to be verified, by the way.

You need that the output is a permutation of the input.

I agree with your larger point though.

Maybe as a last comment, few people actually write tricky concurrent stuff. Like lock-free data structures. There are niches where you gain a lot with a thorough formal spec and verification. But in many cases people should just use sth off the shelf that is already safe, or just use a big lock instead of trying to be smart.

[tombert]

> Thanks for this fantastic extension of my example, because that is still incomplete Input [2, 1, 3] and output [1, 1, 1]. Matches your revised spec, still wrong.

Yeah, I agree with the sibling comment somewhat that you'd probably want to make sure that all the elements are included as well. I do think you'd get much more exhaustive testing at the algorithm level than you'd get with "regular" code, even with unit tests. But sure, your broader point is right, passing the spec doesn't guarantee that everything is "right", and it can be misleading.

I feel like formal methods help when you're optimizing concurrent software more than anything. About a year ago I had a project that I wrote a naive version that was too slow because the initial version had a ton of lock contention. I wanted to rewrite it to use a less lock-heavy system but I wasn't 100% sure that my idea on how to speed it up would actually work. I ended up doing my design in PlusCal before I wrote the new version, and there were issues with my initial version (where in certain cases we could lose vital records), but fortunately I was able modify the design to fix it. I translated my design to Java and my new version was way faster.

I don't agree that a big lock is a good idea, but I do agree that people should, in general, use off the shelf things to handle this instead of trying to be cool. That said, occasionally I get into situations where those libraries aren't a good fit, or what they're doing is too slow.