The point of what I said is that in many cases, lifting a function into a monad means that the code that uses said function can no longer be used to prove what you set out to prove by writing it.

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.