> TLA+ is a formal specification language developed by Leslie Lamport. It is used for designing, modelling, documentation, and verification of programs, especially concurrent systems and distributed systems. TLA+ is considered to be exhaustively-testable pseudocode, and its use likened to drawing blueprints for software systems;
We never enter error state as long as XYZ properties are satisfied, I guess... I will admit, this is probably a naive take, I'm currently trying to go through the TLA+ videos and have trouble wrapping my head around it.
https://en.wikipedia.org/wiki/TLA+
Take something like Google Docs. I'm sure they have some websocket protocol to handle collaborative text editing:
- establish connection
- do a few retries if connection is lost
- always accept edits even when there is no connection
- send queued edits when connection is back
- etc
But what properties can you imagine here?
We never enter an error state? Not really. Error states are unavoidable / outside the control of the system.
We always recover from errors? Not really. Connection might never come back. Or the error requires action from the user (e.g. authentication issues).