Respectfully (you having literally wrote the book!) I disagree that there's a strong difference between specification and programming languages -- and specifically I feel that the "gap" between verification and implementation can be filled by recognizing this.
To take TLA+ as an example -- I've certainly written (short!) programs in both TLA+ and PlusCal -- both imperative (typically an implementation of something that I'm modeling) and declarative (to solve logic problems in the same manner I would use Prolog).
And there's nothing privileged about TLC's capabilities and limitations -- one could equally imagine a TLA+ interpreter which disallows cross-state nondeterminism or use of temporal predicates but allows interaction with the environment via a special variable or predicates, without needing to augment the language, thus allowing "normal" programs to be written and executed. Or a TLA+ interpreter which permits full nondeterminism via a SMT backend, which can act as a richer version of Prolog.
Imagine writing correctness-critical code snippets in TLA+, verifying them, then compiling and linking them into an application written primarily in another language! I don't believe there is anything about TLA+-the-language which would need to change for such a tool to exist.
There are of course language elements specific to verification in TLA+ -- namely the temporal operators pose a challenge to "synthesizing" an executable program. But I don't think this makes TLA+ any less a programming language than the existence of, say, Haskell's type language makes Haskell a programming language.
Verilog sits in a similar space, where it was designed for verification, and is full of constructs usable only for verification, but also has a "synthesizable" subset which can be and is used expressly for implementation without involving verification of any sort. Although one can argue Verilog is a hardware description language rather than a programming language, I haven't seen anyone argue Verilog is a specification language rather than either of those.
You raise good points! Ultimately the technical distinction between a specification and programming language comes down to the existence or not of a compiler. Imagine if Python came out in 1960, but without anybody building a Python interpreter. People would consider it a spec language.
(Also, lots of spec languages are weaker than programming languages, to make verifying them easier. IIRC mcrl2, FDR, and Promela all fall under this category.)
I still think there are practical differences, though, between a language designed for the purposes of specification and one designed for implementing programs. TLA+ has temporal predicates and cross-state nondeterminism because it makes modeling at a high-level easier, even though it makes programmatic implementation harder. That leads to different design decisions through the language.
More importantly to the OP, thinking of them as fundamentally different is useful because they draw on different inspirations. It could be that PLs and SLs converge later, but their origins and lineages are still different. And that's interesting and worth studying.
I don't think talking about ur-languages is as useful as talking about archetypes: "ur-" to me implies "the original", and that's a hard thing to do. TFA has some ur-s like self that aren't the original, but still are useful as archetypes. Off the top of my head, the archetypes of formal speciifcation would be
* Temporal Logic (LTL, CTL, TLA)
* Relational algebra (Z, B, Alloy)
* Guarded Command Language (Promela, SPIN)
* Process Calculi (CSP, FDR)
* Labelled Transition Systems (Petri Nets, mclr2)
* Just drawing a diagram and figuring out the semantics later (UML)
* Abstraction over an existing programming language
This is all real messy, and I see lots of overlapping concepts and unclear cases. Are state machines their own thing, part of LTS, or an implementation detail of the specification approach? Should we be distinguishing between the mathematical formalisms and the languages themselves? What about the vaster world of specifying code and not designs? etc etc etc
Agreed! Phylogeny is messy. And thinking a bit more I realize I'm wading deep into "cereal-is-soup" territory, which is a sure recipe for unhappy diners.
To take TLA+ as an example -- I've certainly written (short!) programs in both TLA+ and PlusCal -- both imperative (typically an implementation of something that I'm modeling) and declarative (to solve logic problems in the same manner I would use Prolog).
And there's nothing privileged about TLC's capabilities and limitations -- one could equally imagine a TLA+ interpreter which disallows cross-state nondeterminism or use of temporal predicates but allows interaction with the environment via a special variable or predicates, without needing to augment the language, thus allowing "normal" programs to be written and executed. Or a TLA+ interpreter which permits full nondeterminism via a SMT backend, which can act as a richer version of Prolog.
Imagine writing correctness-critical code snippets in TLA+, verifying them, then compiling and linking them into an application written primarily in another language! I don't believe there is anything about TLA+-the-language which would need to change for such a tool to exist.
There are of course language elements specific to verification in TLA+ -- namely the temporal operators pose a challenge to "synthesizing" an executable program. But I don't think this makes TLA+ any less a programming language than the existence of, say, Haskell's type language makes Haskell a programming language.
Verilog sits in a similar space, where it was designed for verification, and is full of constructs usable only for verification, but also has a "synthesizable" subset which can be and is used expressly for implementation without involving verification of any sort. Although one can argue Verilog is a hardware description language rather than a programming language, I haven't seen anyone argue Verilog is a specification language rather than either of those.