I’ve been wanting to write about physical and logical time for a while, now I’m sniped ;)

Another important type of determinism is abstraction nondeterminism. Say you’re trying to understand the behavior of a system which makes requests that can succeed or fail. They can fail the requesting server is down, or if it’s online and times out, or the request is malformed, or the requester doesn’t have permission, etc. Even if each of those is locally deterministic from causes, representing the determinism in all of them would get us lost in the specifics of their causes, versus the overall behavior we’re trying to understand. Instead, we can raise the level of abstraction by introducing nondeterminism: requests either succeed or fail.

Some feedback on the specs you wrote:

• TodoMVC should model the state of the todos with a function instead of two sets. Similar to what you did Concurrency, actually.

TodoMVC!Next could me more granular by parameterizing the actions:

Next == \E \in todos:
  /\ AddTodo(t)
  /\ CompleteTodo(t)
  /\ RemoveTodo(t)

For modifying program counters in `Concurrency, I like defining a helper action:

Trans(r, from, to) ==
  /\ requests[r] = from
  /\ requests' = [requests EXCEPT ![r] = to]

SendReq == \* This should be parameterized too
  \E r \in Requests:
    Trans(r, "idle", "fetching")

Man TLC graphviz output could really use a record node option.

That was such a brilliant article. The video completely blew my mind, it’s a total pipe dream become reality. Just seeing someone use tooling that advanced has inspired me to improve my own tooling. I settle for way too little debugging capability.

I think it’s such a good message to apply theoretic concepts like determinism, state machines and logical time to daily programming. These ideas can really a big impact in practical programming.