I wish I knew how to get this point across to people. The way I think of it is that a type-checker which validates a single program at a time isn't capable of proving certain facts which hold when access to filesystems or networks are involved.
All validation is only performed up to an assumed platform.
There's usually little value in worrying too much about how a real platform won't correspond precisely to that assumed platform, since the goal of validation is to remove a class of errors, not all errors.
