Where does TLA+ and PlusCal fit in?
They do not match any of the listed families, do they?
They do not match any of the listed families, do they?
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.
(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
TLA+ is similar to Prolog, extended with a next-state operator and the temporal operators (again, to serve its niche purpose).
(Though the main TLA+ implementation, TLC, doesn't implement logic variables as richly as Prolog does, so coding style within a relation tends to be almost a bit more imperative. They exist in the language though, via the unbounded ∃ operator.)
Looking at some TLA+ examples, I’d say, squinting a bit… somewhere around Prolog ? I’d love to hear someone chip in !
And of course, TLA+ has a suite of temporal operators used exclusively for declaring contracts in service of its role for verifying specifications. Which (as @hwayne points out elsewhere) stem from mathematics -- Linear Temporal Logic specifically -- and not programming.