> Or perhaps the "everything is in the IO monad all the time" nature of imperative code is just fundamentally at odds with code correctness, and we'll always have to fight against it.

In some languages, like D, you can fight against that, by declaring functions to be pure. That's a bit like having everything in IO by default, but marking the exceptions.