I agree with this, but I’m not certain that it’s enough. The problem here is that words like “side effect” imply some kind of abstraction boundary between things that the program should care about, and things that it should not. Without that abstraction boundary, nothing can ever satisfy the conditions to be safe.
In this example, invoking an SMT solver can definitely have side effects if other parts of the program look at the list of running processes to decide whether the SMT solver is running. Does that matter? Most of the time, probably not… but it certainly does matter if you’re using the SMT solver as part of a program that enforces a policy on how many processes a user is allowed to run!
For this reason, I reach the conclusion that Richard’s hypothetical ProofOfSafety is fundamentally impossible to define as part of a general-purpose library, because it relies on decisions about how to draw the right abstraction boundary, and that decision varies from program to program.