[zzzcpan]

Keep in mind, there are different approaches to design distributed systems. You can do pretty much everything without sharing or concurrently accessing any resources, without relying on paxos family of algorithms, etc., it would require you to make sure that algorithms converge, can be retries and so on, but that is local reasoning, easily testable, and it doesn't look like TLA+ even remotely nor can it benefit from it. If you need to model 35 high level steps, your system is definitely not designed that way, is too complex and even philosophically is not in the camp of making distributed algorithms so simple, that they can be easily reasoned about. I guess what I'm saying is that if you need TLA+ you are very likely doing it wrong.

[ones_and_zeros]

> I guess what I'm saying is that if you need TLA+ you are very likely doing it wrong.

Agree to disagree. If your system is distributed it requires you to share data and act concurrently. Otherwise it isn't a distributed system. No amount of retries will cover all of the screwed up things that can happen on an unreliable network.

[zzzcpan]

Sharing data the way you imply is an anti-pattern in distributed systems, you are probably just stuck in a shared memory multithreading mindset. Instead we use specific consistency models. What I described is about models that don't assume that data is up to date on every node but rather operate with the assumption of stale data. And asynchronous networks fail relatively simply too, you are making it the bigger deal than it is. Well, they don't actually fail, but rather this is how they normally operate, they are just unreliable, so you have to assume that data won't be delivered to destinations in time or at all sometimes. If this screws things up for you, then you are definitely doing it wrong. Even if you need low latency, multiple destinations and multiple independent paths is all there is to it, which, again, works well if you don't use consistency models that require consensus. It's like a different world from imperative algorithms with many steps.