Five Kinds of Nondeterminism
Published on: 2025-07-11 22:36:32
February 19, 2025
Five Kinds of Nondeterminism
Or four kinds, or six kinds, I'm not picky about how you count them
No newsletter next week, I'm teaching a TLA+ workshop.
Speaking of which: I spend a lot of time thinking about formal methods (and TLA+ specifically) because it's where the source of almost all my revenue. But I don't share most of the details because 90% of my readers don't use FM and never will. I think it's more interesting to talk about ideas from FM that would be useful to people outside that field. For example, the idea of "property strength" translates to the idea that some tests are stronger than others.
Another possible export is how FM approaches nondeterminism. A nondeterministic algorithm is one that, from the same starting conditions, has multiple possible outputs. This is nondeterministic:
# Pseudocode def f() { return rand()+1; }
When specifying systems, I may not encounter nondeterminism more often than in real systems, but I am definitely more aware
... Read full article.