Sure, but when you make a request to a system you don't control (file system as per the example) all bets are off as far as formal correctness goes. It's beyond

Sure, but when you make a request to a system you don't control (file system as per the example) all bets are off as far as formal correctness goes. It's beyond silly to test for the class of issues that your gp brought up as an example since it would effectively be testing if you wrote malware, which you shouldn't, unless you're a malware author. I get that untested and unaccounted for side effects can feel like malware sometimes, but neither types nor tests will save you from yourself if you act like an unattended dog in a chocolate factory (I count wanton use of side effects to avoid making a clear design decision as such behavior).