A recurring theme in my blog posts is the appropriation of the term “computer program” by Dijkstra and other researchers. The “computer program” concept has acquired at least four different meanings during the course of history. It can refer to:
- a technological object à la Maurice Wilkes in 1950 and Dave Parnas in 2012,
- a mathematical object of finite capacity à la Edsger Dijkstra in 1973,
- a mathematical (Turing-machine) object of infinite size à la Christopher Strachey in 1973, and
- a model of the real world that is not a logico-mathematical construction à la Peter Naur in 1985 and Michael Jackson today.
With regard to Dijkstra and Strachey, see my blog post from March 2013. For Naur's views, see my oral history with him and, likewise, see my interview with Jackson. (Finally, there is of course Raymond Turner's philosophical perspective: to view a “computer program” as a technical artefact, which is not quite the same as Viewpoint 1.)
What I find so vexing is that computer scientists did not consistently follow one interpretation in their writings. Marvin Minsky, for example, used the word “program” on page 25 in his 1967 book, Computation: Finite and Infinite Machines , to refer to data and instructions that fit in a real, finite memory of a physical computer. On page 153, by contrast, the very same word refers to a mathematical object of “unlimited storage capacity,” akin to a Turing machine. Likewise, Tony Hoare consistently used the word “computer” in 1969 to refer to a real physical device but in his 1972 paper the very same word sometimes refers to a finite, physical device and sometimes to a mathematical abstraction in which “infinite computations” can arise .
In sum, historical actors did not always explicitly distinguish between real objects and their models, let alone between all four aforementioned meanings of a “computer program.” In the words of an eminent scholar, “epistemic pluralism is a major feature of emerging fields”  and I have no reason to believe that computer science is any different.
In the next section I present an extract from my rejected POPL paper, pertaining to Minsky's reception of the halting problem. Again, it is the categorical distinction between a mathematical program and a computer program that I wish to emphasize, not to mention the fact that a computer program can be modeled with multiple mathematical programs. Minsky places a “computation system” and a “Turing machine” in the same category. That's fine as long as a computation system denotes a mathematical object. But, later on it becomes clear that he is talking about electronic computers.
Extract from my Rejected POPL Paper: “Marvin Minsky, 1967”
That all being said and done, the anonymous referees [from the CACM] whom I have cited at length [in a previous part of my rejected POPL paper] are in good company for they have history on their side. In 1967 Marvin Minsky reasoned similarly in his influential book Computation: Finite and Infinite Machines, as the following excerpt illustrates:
The unsolvability of the halting problem can be similarly demonstrated for any computation system (rather than just Turing machines) which can suitably manipulate data and interpret them as instructions.
In particular, it is impossible to devise a uniform procedure, or computer program, which can look at any computer program and decide whether or not that program will ever terminate. [8, my emphasis]
How do we interpret Minsky's wordings? Does a “program” solely refer to a “Turing machine” or any other Turing-equivalent mathematical program for that matter? If so, then we could perceive the statement as [completely] abstract and correct; for then it would be a rephrasing of Martin Davis's 1958 account [3, p.70] of Alan Turing's 1936 paper. Or, as a second interpretation, does a “program” refer to a computer program that we can indeed “devise” and that may or may not “terminate”?
Based on a detailed study of Minsky's book, I assert that the right answer leans towards the second interpretation, as also the follow-up excerpt from his book indicates:
(This observation holds only for programs in computers with essentially unlimited secondary storage, since otherwise the computer is a finite-state machine and then the halting problem is in fact solvable, at least in principle.) [8, p.153, my emphasis]
Paraphrasing Minsky, if we view computer programs as Turing machines, then we have an impossibility result with severe practical implications. However, Minsky's reasoning is only valid if the following two assumptions hold (each of which is wrong):
- A computer program is a synonym for a mathematical program.
- The mathematical program (mentioned in the previous sentence) has to be equivalent to a Turing machine program and not to, say, a primitive recursive function.
In other words, Minsky did distinguish between finite and infinite objects, but not between abstract objects (Turing machines) and concrete physical objects (computers and storage), let alone between abstract objects and technical artefacts (computer programs).
The second assumption often goes unmentioned in the literature exactly because computer programs and mathematical programs are frequently conflated. Contrary to what Minsky wrote, a computer with a finite memory is not a finite state machine, it can only be modeled as such.
While I have criticized the first assumption philosophically, the second assumption can easily be scrutinized by having a good look at the history of computer science. Specifically, I will complement the findings of the historians Michael Mahoney [7, p.133] and Edgar Daylight [5, Ch.3] and support the following thesis: computer scientists mathematically modeled actual computations in diverse ways, and many of them did not resort to the Turing-machine model of computation (or to any other Turing-equivalent model). In a word, there never has been a standard model of computation throughout the history of computer science; it is the quest for such a model and not the model itself that brought many computer scientists together.
Revisiting the Gatekeeper
That, then, was an excerpt from my rejected POPL paper. The extract conveys Minsky's 1967 stance with regard to the unsolvability of the halting problem. The question of interest here is whether Minsky intentionally fused the two categories of mathematical programs and computer programs. Perhaps he was merely crafting his sentences with brevity in mind and I am making too much of all this.
My scrutiny of the writings of John Reynolds, Michael Hicks, Andrew Appel, Dave Parnas, Swarat Chaudhuri, CACM reviewers, and Marvin Minsky, at least hints at the possibility that epistemic pluralism is a major feature of computer science too. It is precisely Raymond Turner and like-minded scholars who are starting to lay the philosophical foundations of our emerging field. The POPL Gatekeeper, however, has expressed a very different opinion:
Most criticisms of particular authors and their published claims seem dubious. I think these authors really do understand all the relevant issues and have just crafted certain sentences with brevity in mind. It doesn't work in practice to footnote every sentence with a review of all of its philosophical foundations!
It works to be precise at least once. Conflations abound. Or, to borrow from Timothy Colburn's analysis, here's what Tony Hoare wrote in 1986:
Computer programs are mathematical expressions. They describe, with unprecedented precision and in the most minute detail, the behavior, intended or unintended, of the computer on which they are executed.
This quote, which I have copied from page 132 in Colburn's book Philosophy and Computer Science, is reminiscent of Chaudhuri's words which Parnas and subsequently I, too, have scrutinized. Or, to use Peter Naur's 1989 words, as cited by Colburn on page 147 in his book Philosophy and Computer Science:
It is curious to observe how the authors in this field, who in the formal aspects of their work require painstaking demonstration and proof, in the informal aspects are satisfied with subjective claims that have not the slightest support, neither in argument nor in verifiable evidence. Surely common sense will indicate that such a manner is scientifically unacceptable.
One such subjective claim is, once again, that “full formal verification” is possible; that is,
“full formal verification, the end result of which is a proof that the code will always behave as it should. Such an approach is being increasingly viewed as viable.” — citing Michael Hicks
If the POPL Gatekeeper were to “really understand all the relevant issues” raised in my rejected POPL paper him- or herself, then s/he would either agree with me or with Michael Hicks but not both. The Gatekeeper can't have both ways.
Pluralism is a Virtue
Researching the history and philosophy of our young field already has practical value today. Grasping the multitude of definitions of a “computer program” leads to conceptual clarity and, specifically, to an increased understanding of seemingly conflicting views on computer science. For example the Parnas-Chaudhuri exchange is essentially a clash between definitions 1. and 3., presented at the beginning of this blog post. Each actor associates a different meaning to the term “computer program.”
Appreciating the plurality of “computer program” definitions can lead to better computer engineering practices. For instance, Byron Cook’s article ‘Proving Program Termination’  and Daniel Kroening and Ofer Strichman’s book, Decision Procedures: An Algorithmic Point of View , together present two complementary views on what a “computer program” entails in the present century. For Cook, the variables in the following program text range over integers with infinite precision and, therefore, follow Strachey’s 1973 programming view and show some resemblance with Minsky’s account on page 153 of his 1967 book.
x : = input();
y : = input();
while x > 0 and y > 0 do
if input() = 1 then x : = x - 1;
else y : = y - 1; fi
Kroening and Strichman, by contrast, present an alternative perspective in which all program variables (in the above program text) are defined over finite-width integers and this aligns more with the view held by Dijkstra (1973) and with Minsky’s account on page 25. The implication is that the software tools built by Cook differ in fundamental ways from those developed by Kroening and Strichman. (A descent analysis of Peter Naur’s writings will reveal yet another view on programming.) Good engineers today benefit from this pluralism by using the tools provided from both camps. They will not object if they are requested to use different semantic models for the same C computer program — a point that I have tried to stress before.
 Bensaude Vincent, ‘Studies in History and Philosophy of Science Part C: Studies in History and Philosophy of Biological and Biomedical Sciences,’ 44:2, 122–129, 2013.
 Cook, Podelski, Rybalchenko, ‘Proving Program Termination,’ CACM, 54:5, 88–98, 2011.
 M. Davis. Computability and Unsolvability. McGraw-Hill, New York, USA, 1958.
 Hoare, Allison, Incomputability, ACM Comp. Surveys 4.3, 169–178, 1972.
 D. Knuth and E. Daylight. Algorithmic Barriers Falling: P=NP? Lonely Scholar, Geel, 2014.
 Kroening, Strichman, Decision Procedures: An Algorithmic Point of View, Springer, 2008.
 M. Mahoney. Histories of Computing. Harvard University Press, Cambridge, Massachusetts/London, England, 2011.
 M. Minsky. Computation: Finite and Infinite Machines, Prentice-Hall, 1967.