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

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