Submitted by egdaylight on
I'm reading about “the science of deep specification.” This grand research project is led by Andrew Appel and some other big names on the east coast of the USA. It is only after having read Appel et al.'s on-line research overview again today that I am now 100% convinced that the vast majority of researchers in program verification have not taken the simple objections made by James Fetzer (1988) and Donald MacKenzie (2004) seriously. Again, perhaps they have some very good reasons not to have done so and then I'd like to know why. (By the way, MacKenzie's book also covers some beautiful accomplishments of Andrew Appel's father.)
Andrew Appel and other computer scientists often refer to a computer program while they are actually referring to another representation of a mathematical model of the computer program at hand. I use the term “mathematical program” as a synonym for “mathematical model of a computer program.” So while a computer program can represent a mathematical program, so can
- a text-on-paper representation (called a paper program) and
- a text-on-screen representation (called a screen program)
represent the same mathematical program.
For example, the following is projected onto your screen and therefore it is a screen program:
(defun factorial (n) (if (= n 0) 1 (* n (factorial (- n 1))) ) )
Again, this textual representation, projected onto your screen, is a representation of a mathematical object, i.e., a mathematical program. (One can perhaps also say that it is a textual representation of a computer program. I definitely take no issue with that viewpoint. But, in order to avoid confusion, I will not use the verb "to represent" in that manner.) One might be tempted to say that the textual representation is a computer program. This is frequently not a problem but it is in the current setting where formal methodists, themselves, want us to be merciless precise. So let's indeed try to be crystal clear.
The paper program, the screen program, and the computer program are three different representations of the mathematical model. (They are three different technical artefacts.) The first and second representation, intended for humans to read, are very different from the third. A computer program resides electronically in a specific computer and is (a) what we all would like to get “correct” and (b) what we all have difficulty comprehending because it is an artefact engineered for a digital machine.
Coming now to Appel et al.'s research overview. The authors state that
Until recently "program verification logics have not been `live:' they have been about models of the program."
But any mathematical endeavor such as program verification can at best be about mathematical models of the engineered system at hand. That system, in turn, can contain one or more computer programs. Each computer program can be modeled in one or more ways by a mathematically-inclined researcher. Likewise, one can mathematically model a running computer program by resorting to, say, an operational semantics of the computer program under scrutiny. But how can mathematics become `live'? What, exactly, is this supposed to mean?
Continuing with Appel et al.'s words:
Program verification logics are now “connected directly and mechanically to the program”.
Notice that Appel et al. oftentimes use the word “program” (such as the last word in the previous sentence) as an abbreviation for “computer program” — i.e., the real mechanical stuff. But the first occurrence of the word “Program” in the previous quote has to refer to a mathematical program! For, how could you prove a logical statement without having a semantic model of the engineered computer program? Or, to be more precise, the first occurrence of “Program” has to refer to a textual representation of Appel et al.'s chosen mathematical program while the last occurrence has to refer to an electronic — humanly unreadable — representation, i.e., a computer program.
In other words, the authors conflate their textual representation of their mathematical program and an electronic representation of that same mathematical program (i.e., the computer program that we all want to get “correct”).
Appel et al. are basically saying what John Reynolds and Michael Hicks have said before, namely that full verification of a hw/sw system is possible, both in principle and in practice. My claim is that this is not possible in principle but that program verification nevertheless does have a lot to offer in practice, especially if formal methodists will get their terminology right when disseminating their research findings to, say, software engineers in industry.
Continuing with the words of Appel et al.:
“we envision this network of verified software components, connected by deep specifications—specifications that are rich, live, formal, and two-sided.”
Some of these italicized words I do not understand at all but perhaps it's just me. Continuing:
“whatever properties are proved about a program will actually hold when the program runs”
This latter sentence exemplifies a category mistake, essentially already pointed out by Fetzer in 1988 and refined by me as follows: One can mathematically prove a mathematical property on a mathematical model of a computer program. One cannot prove a mathematical property on a computer program, regardless of whether the latter is running or not. So the first occurrence of “program” in the previous quote refers to a mathematical program while the latter occurrence — “the program runs” — has to refer to a computer program.
To conclude, Appel and his fellow researchers fuse the category of mathematical objects (which includes mathematical programs) with the category of engineered systems (which includes computer programs). Perhaps there are very good reasons to do so and I am merely demonstrating my ignorance. In any case, the `science of deep specification' remains intriguing to me because I am not even able to grasp some of its basic principles.