Enjoyed this. The underlying formalism seems based (I think?) on concurrent, independently-executing processes that are stimulated by messages. That has some similarities with the Actor model [0], albeit Actors support concurrent, intra-process message handling whereas this seems sequential at the individual process level. So maybe more like Communicating Sequential Processes [1].
For anyone more knowledgable on the topic: is that right? And is that model common across other proof systems like TLA?
Second (bonus) question: why separate messages from user input?
> And is that model common across other proof systems like TLA?
Yes, it's pretty common, and is a really nice abstraction.
TLA+ doesn't use that model, although a lot of TLA+ code is implemented that way. TLA+'s model is basically "shared memory" where any step can access or change any state in any way it likes. That's super flexible, but can feel a little too flexible.
P, on the other hand, is based on a model of state machines that communicate with messages. See this example for a clear illustration of how that works: https://p-org.github.io/P/tutorial/twophasecommit/
For anyone more knowledgable on the topic: is that right? And is that model common across other proof systems like TLA?
Second (bonus) question: why separate messages from user input?
Thanks.
[0] https://en.wikipedia.org/wiki/Actor_model [1] https://en.wikipedia.org/wiki/Communicating_sequential_proce...