One of the features of some next-gen projects is to eliminate the need for techniques like TLA+ and UML. The concept is to make the specification the final code, and skip the implementation phase. Since TLA+ and UML do not produce a final product you have then the errors related to mapping those into executable code. In my own work i go from sketch, to data structure design, to executable spec which is the final product. I believe that is the shortest way to the goal.

Is an executable spec a programming language that looks spec-like?

yes, an executable spec is just a very concise programming language that leans towards the declarative, and has a minimum of "fat" in terms of extraneous words. I measure projects by how many words are typed into the computer, as line count is highly misleading due to some languages being more vertical than horizontal. I consider spec-only languages to be a giant waste of time because with almost the same level of effort you can build the product, so why bother with a non-executable intermediary? The other objection i have with TLA+ is that it doesn't include a graphical model, and since the majority of words of code in a typical graphical interactive product relates to drawing, specifications which don't cover visual appearance are thus only partial specifications, and not conducive to improving productivity.