I agree in principle, but there’s a rather fundamental problem here: writing the spec has to be easier than writing the program. Otherwise,we should just write a compiler for the spec language and save ourselves a step, or blunder on by writing the program without a spec, as is usually done.
I think if you're doing your spec as a combination of high level set theory or algebra and some prose, then it should be easier than writing the program itself (assuming you know a bit about math and how to write a spec).
The question is how much time is it worth putting into writing a detailed spec. I think the answer is that it really depends on the size and complexity of your software.
I think the idea is that programmers have to be comfortable with writing something down, even if it's not perfect. A half-baked spec is better than no spec, basically. Otherwise you will likely end up with spaghetti code that needs to be rewritten or scrapped.
Writing a useful TLA+ spec will usually be easier than writing an operational program with the functionality the spec describes, because it lets you abstract over the uninteresting parts.
It pushes the bugs to things that are easier to test. You write tests for things like "we properly error on a malformed input" and write TLA+ specs for things like "there are no awful concurrency bugs spanning three servers in two regions."
