I'm not talking about phantom types/ghost variables, and I don't mean "not compiled" but cannot possibly be compiled or not compileable. You can easily write non-computable specifications in TLA+, and it's useful! (e.g., to state that a certain program decides halting in certain circumstances). You can also very easily define things like being in NP with angelic nondeterminism. Many interesting and useful things you can say about a computation cannot themselves be compiled to computations.

> There is a lot of overlap between the things you want to do with specifications and the things you want to do with executable code

Sure. Programs are a special case of specifications. TLA+ easily expresses both. The tradeoff is this: is every specification of an algorithm compilable or not? While TLA+ can easily specify algorithms at any level of determinism, not ever specification of an algorithm is compilable -- i.e., some may be too nondeterministic. For example, even Quicksort is not-compilable. Quicksort implementations that can run (i.e., those expressed as programs) do not actually specify Quicksort, but particular refinements of it (see https://pron.github.io/posts/tlaplus_part3).

> So to my mind there's a lot of value to be had from a language that integrates specification and executable and is able to express both.

As I said above, TLA+ easily expresses both (in fact, there are research tools that compile C and Java bytecode to TLA+). But to guarantee compilability you must demarcate the executable part (a language like, say, Agda, does this with a formal separation between types and "terms"; Java+JML does this with a formal separation between code and specification). So as to languages that are made of two sub-languages -- one that affords arbitrary nondeterminism and one that can always be compiled -- sure, that has a value, but that value comes at an extremely steep price. Sometimes that price may be worth it; sometimes not. Not to mention that even those languages rarely achieve TLA+'s strengths, because very often TLA+ is used not to specify a particular executable, but a whole system (which includes multiple executables and their environment). In those very common cases the ability to compile becomes pure cost.

What TLA+ shows is the great value in giving up the ability to compile every specificaton -- an extremely expressive specification language that can be easily learned and used. I've written someplace else (https://www.reddit.com/r/tlaplus/comments/abi3oz/using_tla_t...) that TLA+ might well be the first rich formal logic (as opposed to programming languages that have no quantification) in the history of formal logic that is actually used by practitioners whose job isn't to use formal logic all day (or have been trained in formal logic for a very long time) -- in effect, the first to achieve formal logic's stated goal as a simple tool for practitioners. A goal that has been abandoned by logicians very early on.

In TLA+, you could write a realizable implementation of Quicksort, but also specify Quicksort itself and show that any implementation works. You could do the same in, say, Agda (or Java+JML), but at a much higher cost. TLA+'s power is in being extremely expressive, and at the same time extremely simple (never mind Agda - it is simpler than Python).