In my experience code quality falls out from making mental simulations easier to produce. Abstraction boundaries should be drawn where mental processing starts feeling burdensome.

When running abstract mental simulations, do you assume that I/O operations succeed or fail for knowable reasons? It seems likely. If the code were expressed to match your mental simulation, for example by not performing I/O within the function, but by merely receiving I/O messages from a foreign actor, it seems like you're not far away from offloading the full mental simulation to something like quickcheck and writing down explicit invariants!