Effects like I/O have to be explicit: code that wants to do I/O has to be passed an object that can do I/O, it doesn't get any such objects by default at the time it's loaded. Besides this means of control ('capability security') there's also an 'auditors' mechanism for static analysis, e.g. to require some code to have no side effects.

(I'm not endorsing the GP comment; it's not how I would've phrased things. The auditing mechanism does enable proofs, but it was relatively new and experimental, compared to the core capability-security ideas.)

Added: http://erights.org/talks/auditors/index.html