Earlier quoted context omitted.
I agree with your comment in general, however I would say that on my field, the resistence to TLA+ isn't having to think, rather having to code twice without guarantees that it actually maps to the theorical model. Tools like Lean and Dafny are much more appreciated, as they generate code from the model.
But both Dafny and Lean (which are really hard to put in the same category [1]) are used even less than TLA+, and the problem of formally tying a spec to code exists only when you specify at a level that's much higher than the code, which is what you want most of the time because that's where you get the most bang for you buck. It's a little like saying that the resistance to blueprints is that a rolled blueprint mak…
That is not the case for the TLA+ spec and your 1MLOC Java Database. You hope with fingers crossed that you've implemented the design, but have you?
I can measure that a physical wall has the same dimensions as specified in the blueprint. How do I know my program follows the TLA+ spec?
I'm not being facetious, I think this is a huge issue. While Dafny might not be the answer we should strive to find a good way to do refinement.
And the thing is, we can do it for hardware! Software should actually be easier, not harder. But software is too much of a wild west.
That problem needs to be solved first.