An example why verified programming is hard.
Walking back from where I parked my car today, I realized how difficult it is to make sure specifications are satisfied, once you start looking at them formally. There are specifications with obvious meanings, and obvious algorithms to satisfy them. But ...
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.
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.