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

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