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