Yes, exactly: a function that requires a volatile (or IO) annotation is one for which (some of) the things you could use a non-volatile function to prove are no

Yes, exactly: a function that requires a volatile (or IO) annotation is one for which (some of) the things you could use a non-volatile function to prove are not actually true. If you want to lie to the compiler[0], unsafePerformIO, seq, and other unsound primitives are available and documented. Contrariwise, if you want to not lie to compiler, the primitives for that are also available and documented. 0: Which is a completely resonable thing to do, and the basis of any language's standard library, the ability to recapitulate which in normal code separates good languages from Go-like special-cases-for-me-but-not-for-thee languages.