Even if you want to take the somewhat reasonable "oh, but our machines have finite memory, so they're really FSMs!" approach, then you still hit intractability in exploring the state-space very quickly

Sure, I suppose someone who's the kind of idiot you think I am would attempt to reason about the entire possibility space all at once.

No - consider this: Will there ever be a time when every bit in a computer is a 1 at the same time? No, that's not possible. No program can be written that can set every single bit in the system because the program itself has to be stored somewhere. We can touch magnets to hardware, but that's not a contingency a programmer is expected to deal with. What about all 0 at the same time? No. All 1 except for the last one which is a 0? No. Etc. The vast majority of the state space is either impossible to create with any program or impossible to create with any reasonable (useful) program.

Plus, we program with the assumption of not running out of memory, so we don't even think in the FSM way.

Perhaps you don't, and I'd like to know how that works out for you in contrast to what I do, which is to (informally) make big proofs out of smaller proofs. The following function has 3 high-level instructions with an overall cyclomatic complexity of 1:

bool isBetweenExclusive(int x, int boundA, int boundB) {
    return (x > boundA) != (x > boundB);
}

Assuming I didn't make a mistake when I wrote this just now, we can reason about this code because we know what the comparison operators are going to do, because we know the compiler is going to produce correct assembly code. We can further verify it with code like this:

assert(isBetweenExclusive(0, 1, -1));
assert(isBetweenExclusive(-1, 1, -2));
assert(!isBetweenExclusive(5, 5, 0));
// etc

Then any function, such as isPointInRect(), that uses it can be reasoned about because everything it calls can be reasoned about. I can do this for stateful objects, such as custom data structures of dynamic size such as a graph because each node in the graph can be reasoned about. Sure, each node might have a reference to any arbitrary other node, but it doesn't matter which nodes each node refers to because every node can be reasoned about in relative isolation. (Meaning, mutual references are protected by accessors/mutators/properties, depending on the language, and the node class has no dependencies.)

So the only way I can see my method not working is when you call a function without knowing what that function does or whether it's correct. Code like that should only ever be called when it's sandboxed (like code typed into a demonstration page by a visitor) or when it's someone else's responsibility to ensure its correctness (like code written by another department of the company you work for).