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 of its presence. Modeling nondeterminism is a core part of formal specification. I mentally categorize nondeterminism into five buckets. Caveat, this is specifically about nondeterminism from the perspective of system modeling, not computer science as a whole. If I tried to include stuff on NFAs and amb operations this would be twice as long.
1. True Randomness
Programs that literally make calls to a random function and then use the results. This the simplest type of nondeterminism and one of the most ubiquitous.
... continue reading