First of all, you're assuming that the person who writes the theorems is always correct and is able to describe their code accurately. This is not the case. Second, it's way more easy to take a bunch of common sense measures than to deal with this.
No I'm not. When I say "no error", that include the specs. For instance, correctly following a specs when the green button set of the emergency shut down makes the interface too astonishing. That's a bug.
> Second, it's way more easy to take a bunch of common sense measures than to deal with this.
Of course. we never tried it seriously. What we didn't try yet is always more difficult. But if we do, it may very well become easier. I don't know.
Anyway, these weren't the point. My point was that the domains where we need bug-free code is broader than we might think at a first glance. Not being able to trust that the code you run is error-free has costs that could very well be more important than taking the time to prove the absence of errors.