I think your question really is, could one design a programming language -- i.e. a language where everything is executable -- inspired by TLA+? The answer to that is absolutely! Someone here mentioned Quint, which is also intended for verification, but works much more like a programming language, and is inspired by TLA (the temporal logic in TLA+). Microsoft Research's P programming language (https://p-org.github.io/P/) could be said to be such a language, and I recall seeing several one-person attempts whose names I can't remember. There are also temporal-logic- based programming languages that precede TLA+, like Esterel (https://en.wikipedia.org/wiki/Esterel).

> as soon as you say it realizes unrealizable things, you are speaking poetry rather than programming language design

No! Because the purpose of TLA+ is not to build executable things but to help design and reason about executable things, and it turns out that being able to describe non-executable things is very useful for that purpose (as I tried to show with the Halts example). The ability of a mathematical specification language like TLA+ to describe unrealisable things is the source of its power to succinctly and clearly specify realisable things, because a description of something is not the thing itself.

It's like saying I'm not interested in mathematics, only the subset that can describe physical things. But it turns out that restricting mathematics to physical things makes it more difficult to work with.

This isn't poetry, just the practical realities of mathematics.

> TLC

I think your focus on TLC is a distraction because even when your TLA+ specification does describe a computable process, TLC doesn't actually run that process (it can be put in a mode that does, but that's actually more confusing here). TLC behaves more like a sophisticated type-checker. Type checkers are extremely useful (and TLC even more so) when reasoning about a computational system, and some clever people have found ways to program them to produce interesting outputs, but that's not really what you have in mind when you think about running a program.

For example, TLC can check and verify in an instant a specification of an uncountably infinite number of executions, each of infinite length, and yet choke on a specification of only a few possible instances of, say, QuickSort.

> it seems clear you are talking about a level beyond this, where a TLA+ specification cannot be evaluated even with symbolic tricks.

Yes, but even that is not the point. You seem to be very focused on execution, programming, and evaluation, and these are not the things that TLA+ helps with.

There is no doubt that a programming language is more useful than a mathematical specification for producing software -- because you can build software without a mathematical specification but not without a program -- just as a hammer is more useful than a blueprint when building a cabin, as you can build the cabin without a blueprint, but not without a hammer. But asking how to fashion the blueprint into a hammer misses its point.

Consider this mathematical description of the vertical motion of a projectile thrown from ground level:

    y = v0*t + 0.5gt^2

You can certainly numerically evaluate this formula at different points to create a simulation and plot its motion, and that is very useful, but it's not nearly the only useful thing you can do with the formula. By applying mathematical transformations on the formula (without evaluating it) you can answer questions such as "at what speed should I throw the projectile so that its maximum height exceeds 10m?" or "at what speed should I throw the projectile so that it hits the ground again after exactly 5s?"

The purpose of TLA+ is to write a small specification of the relevant details of a 5MLOC program, and use it to answer questions such as "can network faults lead to a loss of data?" Sure, running the program is the ultimate goal, but being able to answer such questions can be extremely helpful, and is hard to do with a detailed description that's 5 million lines long.

Now, it's perfectly fine to say that you don't care about such capabilities, but these are the capabilities that TLA+ exists to give.

There are languages out there that aim to do both -- produce an executable and offer advanced reasoning capabilities -- but these languages usually turn out to be much more difficult to program with than traditional programming languages and harder to reason with than with TLA+.