 A second theoretical difficulty concerning proofs of correctness for computer programs concerns their complexity and that of the programs to be verified. Already Hoare (1981) admitted that while verification of correctness is always possible in principle, in practice it is hardly achievable. Except for trivial cases, contemporary software is modularly encoded, is required to satisfy a large set of specifications, and it is developed so as to interact with other programs, systems, users. Embedded and reactive software are cases in point. In order to verify such complex software, correctness proofs are carried out automatically. Hence, on the one hand, the correctness problem shifts from the program under examination to the program performing the verification, e.g. a theorem prover; on the other hand, proofs carried out by a physical process can go wrong, due to mechanical mistakes of the machine. Against this infinite regress argument, Arkoudas and Bringsjord (2007) argue that one can make use of a proof checker which, by being a relatively small program, is usually easier to verify.