He stirred up a debate that lasted quite some time and involved many prominent Computer Scientists, however the essence of Fetzer's position, and an adequate refutation can be stated in very few words.

Fetzer's position was that to claim to have formally verified a computer program is to claim to have mathematically proven that a computer executing that program will always give correct results. Since this is a claim about the contingent behaviour of physical objects, it is an elementary epistemological error to suppose such claims susceptible of logical or mathematical proof. I believe that Fetzer also asserted that a computer program is a physical object, and that this may have been why he though a claim to verification must be contingent.

Fetzer was wrong in the most elementary way. Computer scientists who talk about program verification are making no unconditional claim about the behaviour of physical machines. (you could say that provided the computer conforms to its specification it will obtain the correct results when executing the program, but in fact no reference to computers is necessary or desirable).

Not only is Fetzer's position based on a misunderstanding of the language of computer science, it also reveals a gross underestimate of the philosophical sophistication of the average computer scientist.

I have myself participated in work related to program verification, and including hardware verification. When I first became involved in hardware verification this area was not widely understood even by computer scientists familiar with the idea of program verification. It was not uncommon for me to receive puzzled enquiries from people who understood how program verification might be possible but could not understand how hardware could be verified. Computer Scientists are all too aware that computers, even when their design is without flaw, sometimes do not behave as they should.

On the question of whether a program is a physical object, the terms hardware and software dating from the earliest days of computing, testify to an awareness that the former but not the latter consists of physical objects.

© created 1996/2/26 modified 1998/7/30