Comment by brazzy
1 day ago
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.