This is a good list but is almost more accurately called a list of modeling languages.
At the very least it’s a very particular interpretation of specification, which makes sense from a TLA+ expert but is incomplete.
In particular I think there are a few candidate ur-specification languages that could be included:
* first-order logic, this captures what almost every deductive verifier uses, and has a surprisingly rich diversity in features.
* concurrent separation logic, this was a breakthrough development and every language for specifying concurrent programs is some flavor of this now.
* dependent type theory? The big issue is that as the author points out, taxonomies fail. Dependent type theories give rise to languages which are both “specification” and “programming” languages.
Based on the state of academic conferences in formal methods, I would have 4 languages: temporal logic, first order logic, concurrent separation logic and dependent type theory. This categorization provides generalizing powers because tools, techniques and limitations mostly map onto it.
* temporal logic: almost exclusively used by model checkers. Usually propositional, has limited/no support for quantifiers. Also usually only able to express path properties. This for example makes it hard to state “is_sorted”.
* first-order logic: used by deductive (semi-automatic) verifiers. Can reason about complex properties of state (ie : `is_sorted`), harder but not impossible, to reason about temporal properties. Ill-suited to describe properties involving shared state or concurrency. Used by SMT solvers in particular (good automation). Also used by most deductive verifiers and liquid type systems. Examples: Dafny, Why3, SPARK (spec part), liquid Haskell.
* concurrent separation logic: can be either propositional, first-order or higher order. Does much of the same kinds of properties as FOL, but it can reason about shared state and concurrency, in fact it’s quite good for that. This expressivity usually means it’s harder to reason about / prove specifications. Examples: Iris, Viper, Verifast.
* dependent type theory: when you start pondering what it even means to specify something, the gods of CS bestow upon you a vision of the haskell-curry isomorphism and your programs become specifications and your specifications become programs. This is the “ultimate” level of specification, and the foundation for proof assistants. Examples: Coq, Lean
Each of these categories is well represented at conferences and pretty much every paper falls into one of these four buckets. These also map roughly onto verification methodologies and problem domains.
On second thought, these are mostly too closely related, I think that if you want to truly find the ur-specification languages this is closely related to Girard's research program. Specification languages are intrinsically tied to a notion of truth and also of proof (method of establishing / showing truth), these are central questions in Girard's work.
I think a revised list should also include proof-nets, and other weirder specification languages like the [flower calculus](http://www.lix.polytechnique.fr/Labo/Pablo.DONATO/drafts/FJ....) or stellar resolution. These also stretch the usual interpretation of language as a syntax tree.
In particular I think there are a few candidate ur-specification languages that could be included:
* first-order logic, this captures what almost every deductive verifier uses, and has a surprisingly rich diversity in features.
* concurrent separation logic, this was a breakthrough development and every language for specifying concurrent programs is some flavor of this now.
* dependent type theory? The big issue is that as the author points out, taxonomies fail. Dependent type theories give rise to languages which are both “specification” and “programming” languages.