After passing the hospital front door, I decided to park in the first available space. The obvious way to do this is to keep driving until I see an available space, and then park in it. But, when I'm finally parking in that space, is it the first available space? Can I know that? When I walked back to the hospital, I saw another available space. It hadn't been available when I drove past it. Was it there when I entered my parking space? I have no idea.
Now this is everyday trivia. But if something like this were to happen in a computer program, and other formal reasoning depended on getting into the first available space, things might get difficult. Would I have to make the specifications weaker? Would I have to make it precise in a complicated way? Would I have to change other code that depended on the details of the spec I could not implement?
Formal verification is hard. Informal verification is impossible. We resort to debugging, and our systems are are vulnerable to attack.