3 ms·
I think he meant to write deterministic. The exact nature of the logic TLA is not the relevant point here. TLA (and so TLA+) extensively relies on nondeterminis
by pron 7y ago
I think he meant to write deterministic. The exact nature of the logic TLA is not the relevant point here. TLA (and so TLA+) extensively relies on nondeterminism for things like specifying code at arbitrary levels of detail (e.g. you can say, after this step, the list is sorted somehow, without specifying how), interaction with the environment (the user performs one operation of the possible ones, or some arbitrary machine fails) or concurrency in its programming sense (the OS will schedule one of these several operations next).
- zozbot234 7y agoI agree, mostly, but understanding "the exact nature" of a logic (or at least a properly-defined subset of it) is pretty important for using it effectively.
- pron 7y agoIf you're interested, I've written a rather detailed explanation of the TLA+ logic. Part 1 is an introduction that explains the design from a UX perspective, part 2 is about the + side of the logic, and parts 3 and 4 are about TLA: https://pron.github.io/tlaplus https://pron.github.io/tlaplus