The feasibility of automatic verification and ease of specification played incredibly important roles in the historical development of specification languages.

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 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.