First of all, our model of computation can be too abstract. We end up having a granularity which does not allow to capture the details of the concrete system we have at hand. The second limitation is that the specification that we are using may be incomplete and this indeed was the case in the first concrete and extended example that was carried out of the formal verification of a processor. This was the case of the Viper micro-processor where indeed it had been completely formally verified but in the end it did not work because the verification had been made against the specification which was in fact not what the concrete physical object was about. But there is a third kind of limitation which we are more concerned here.
That is that proofs themselves may contain errors. And why is that the case? Well carrying out a formal derivation by hand is a very tedious activity. One has to check many thousands of steps often. And most of these are trivial. And because of this triviality rather than making the task of formal checking easy it makes it even more confusing. And so our response, the response that we are advocating in this course is not exactly that of theorem proving but it is that of assisting in proof development. The computer is supposed to work as an assistant who deals with all the tedious and tiny details and helps you not to lose your bearing while you are carrying out a proof, making sure that you have not missed all the cases that you want to check. It is not going to help you in the crucial steps. There it is still your ingenuity that will have to be used. It is still the provers ingenuity intelligence that suggests the crucial steps. But all the trivial steps and especially all the bookkeeping which is obviously involved in carrying out a formal proof, all that is taken care by the computer.
