I'm not sure how they do it, but I would be tempted to have some static analysis at save time. The static analysis can't be perfect in a Turing complete langua

I'm not sure how they do it, but I would be tempted to have some static analysis at save time. The static analysis can't be perfect in a Turing complete language embedded in an environment that admits impurity, but it can be proven conservative so that no impure methods are falsely marked as pure at save time. I've done something similar for commit-time code analysis to generate an error if a proven non-negative seed is passed to a Numerical Recipes in C-style random number generator (non-negative seeds silently ignored). Alternatively, if the interface to the OS itself is small enough, they could run their tests in a sandboxed environment where all methods to access the file system, network, clock, etc. are replaced with stubs that throw exceptions.