I think one of Lamport's arguments was that at specification level one shouldn't go for an imperative approach. Imperative is good for "how to" instructions (programs). Declarative is good for "what is" or "what should be" instructions (specifications). So in that sense TLA+ was about helping you build state machines via simple declarative syntax. Of course this was Lamport's argument, in practice, your approach may work just as well. Will definitely be interested to see how your approach evolves.
This kind of argument aren't new to formal methods. They have been present ever since high level programming language came to existence.
Functional programming proponents have always argued how great functional languages are and how natural they are and how elegant their programs look. However, what really matters is what gets the work done.
From my understanding of the history of programming, people will always resort to multi-paradigm solutions. For programming, they will use objects oriented concepts, sprinkle with imperative code within their classes, occasionally use functional programming when that is actually elegant.
Despite that, TLA+ ended up having PlusCal which is almost an imperative style (not actually imperative) language.
Comments
I think one of Lamport's arguments was that at specification level one shouldn't go for an imperative approach. Imperative is good for "how to" instructions (programs). Declarative is good for "what is" or "what should be" instructions (specifications). So in that sense TLA+ was about helping you build state machines via simple declarative syntax. Of course this was Lamport's argument, in practice, your approach may work just as well. Will definitely be interested to see how your approach evolves.
This kind of argument aren't new to formal methods. They have been present ever since high level programming language came to existence. Functional programming proponents have always argued how great functional languages are and how natural they are and how elegant their programs look. However, what really matters is what gets the work done.
From my understanding of the history of programming, people will always resort to multi-paradigm solutions. For programming, they will use objects oriented concepts, sprinkle with imperative code within their classes, occasionally use functional programming when that is actually elegant.
Despite that, TLA+ ended up having PlusCal which is almost an imperative style (not actually imperative) language.