The feasibility of automatic verification and ease of specification played incredibly important roles in the historical development of specification languages. This raises an interesting question: what new computational tools are coming on the scene, and what role will those tools play in the next generation of specification/programming languages?
Reading this article, I was struck by how noneterminism was all over the place in ur-specification languages. I think the answer to the question above will turn out to be something about: 1. nondeterminism, and 2. LLMs, RL, and diffusion as a way of resolving/refining nondeterminism.
That aside, I like the taxonomy. Some personal footnotes:
1. I would list Hoare Logic as the ur-language instead of GCL. Dynamic logics are in this family. I had never considered Spin and dynamic logic as being related in this way. That's kind of neat, and I'm glad I read the article.
2. I would probably give type theories a place in the list, even though you have to squint a little bit to make them fit in a list of specification languages.
3. The history of temporal logics is fascinating, and https://www.cs.rice.edu/~vardi/papers/etaps01-ver13.pdf is probably on my top ten list of papers on formal methods.
4. I feel exactly the same way about Petri Nets -- kind of neat, feel powerful, but never quite know what to do with them. Maybe now that we're returning to office I will get a copy of "Petri Net Theory and the Modeling of Systems" for the train ride.