In this case, the sanity-checking-before-operation does not help satisfy the post-conditions, because between the time you check for sanity and the time you actually do the operation, things may change (see TOCTTOU). In other words, the post-condition of sanity-checking is not sanity!

Sanity-checking doesn't help the system satisfy its post-conditions, therefore it doesn't make sense to require it as a pre-condition. It's okay to do sanity-checking to save users' time, but you MUST NOT rely on it for correctness.

EDIT: I read this as saying you're using the sanity-checking for proving correctness, but Nominal Animal reads the opposite. So I guess at least one of us doesn't "see what your sayin"

I do agree. You can see from my shell script suggestion that I prefer to do the pre-checks (like checking if the user exists) too -- I just felt it was important to emphasize one must not think the pre-checks replace run-time checking. The check prevents a doomed attempt, but I do not rely on it: the actual file/directory tests later on will fail gracefully (with the correct logical result) if the user vanishes in the mean time.

(EDIT: Ntubski, you're preaching to the choir. I understood from ph0n3s description that he is not relying on sanity checks before/after for correctness.)

Using pre-checks in an effort to avoid having any kind of error checking during the operation itself is a very prevalent programming technique, and one that really, really irks me. I honestly thought that that was what you were doing, but I guess I was wrong; I apologise. Not only is the technique unreliable (EDIT: as Ntubski mentioned, due to TOCTTOU), because the situation may change at any point, but it also makes it very hard to track the algorithmic restrictions (since they are never tested during the operation). It makes code maintenance much harder in the long-term, and in my experience, always leads to severe bit-rot. The code quality degrades severely over time, as additions and changes are made. The only reason for it, as far as I can see, is pure programmer laziness.

Properly written code that checks for errors is easier to maintain, because you can simply read the code to find out which situations it can and cannot handle. Optimally, the comments should explain the assumptions and requirements for each situation, so later developers get the correct mental picture.

My own coding style is very defensive. (My comments still need a lot of work; I still tend to document what the code does instead of what the intent of the code is. I'm working on it.) For example, when using low-level I/O (which I use a lot, for minimum overhead), I check read() and write() return values for negative values other than -1. They should never occur, and I've felt a bit foolish doing that for years. Recently, a colleague found one case where they do, and it is a kernel bug. (It only occurs with 2.6 series kernels and over 2GB vectored writes on x86-64 using ext4.) The test is essentially free (one if clause per I/O syscall is irrelevant wrt. performance), but I have not seen other code that does that test.

I am not familiar with formal verification methods. I've never worked with software that has required those. Currently I mostly work with molecular dynamics simulations, where the simulation itself may sometimes get unphysical (completely bonkers due to limited precision or invalid starting values, or for other reasons), and it is pretty important for the simulator itself to catch such states. Most computational physicists learn early on to look at the simulation overall to determine if it makes "physical" sense, or is completely unphysical and thus more or less garbage, but sometimes such situations may be disguised or last only for a short time. I find it is much better if the simulation stops, instead of assuming the user catches any errors.

My point is that even if formal verification is too big a hammer for all software in general, programmers should be pragmatic and accept that shit happens way too often, and make sure their software just deals with it the best way it can. Checking if the dung has already hit the fan is not enough; it may happen at any point in time, even if you just checked for it a nanosecond prior. It makes business sense, too. People don't really remember successes that much, but they sure do remember spectacular failures.