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