Comment by caspper69
1 day ago
The article wasn't bad, but the examples felt a bit thin; almost like the author was reaching a bit to hit that magic number of 5.
And you're definitely not wrong on the abstract subsection. I mean, essentially all he says is that "there's a mechanism in our system which is so complicated/convoluted that we decided not to model it with TLA, so instead we chose to simply call it non-deterministic, and therefore it is now abstract non-determinism." Hmm. If we're truly being abstract, that's not really all that different from the PRNG and user input examples, except, you know, it's actually still completely deterministic code.
Also, I have to say- 5 different types of non-determinism, and not one mention of quantum systems?
I took issue with #4 too. If your code consumes API endpoints that are non-deterministic, that strikes me as something you should take up with your vendor. An error condition on a network call is not non-determinism. It's just reality from time to time.
The author is writing on the context of formal verification. From that point of view, modelling an error condition on a network call as non-deterministic and just lumping potential bugs in the remote API into that as well since you don't control it (i.e. it is not part of the system you are trying to verify) just makes sense so you can go forward with verifying that your code will do the right thing no matter what happens.
Understood. It was hard to tell if he was only writing it from the standpoint of FM or if he was speaking more generally.