Submitted by egdaylight on
Dated:
In 2006 I defended my Ph.D. thesis at KU Leuven. Dr. X from abroad was in my defense committee. He had taken the liberty a few days earlier to share with me some of the "fundamental limitations" he had found with regard to transformational systems, such as the system I had designed, implemented, and documented for my Ph.D. defense. (A comprehensive overview of my system later appeared in Science of Computer Programming [1]). Dr. X had already published his theoretical insights and he wanted me to incorporate his findings into my Ph.D. dissertation.
I had to follow a Master of Logic program at the University of Amsterdam (2007-2009) to actually start understanding each and every argument in Dr. X's theoretical paper. My incentive to do so was because I intuitively felt that Dr. X's reasoning was flawed. In the process, and due to my strong interest in the history of ideas, I started to see that several computer scientists, including the most prominent ones, had been making and were continuing to make "category mistakes" like Dr. X.
Very briefly: Dr. X's point was that he had mathematically proved that certain systems cannot be engineered. That is, mathematics and computability theory in particular prevail over engineering and all engineers better start learning computability theory. I believe I am today in a position to improve the wordings of Dr. X with regard to his own article. I would say that:
If I model my transformation system with his Turing-machine formalism, then I obtain a classical undecidability result from computability theory which gives me insights into the industrial problem that I and fellow engineers are trying to solve.
The undecidability result does not tell me that specific systems cannot be built. That being said, a good engineer could or perhaps should (with an emphasis on "perhaps") take the undecidability result into account when engineering systems.
Dr. X's view on undecidability and its alleged implications on practice are also strongly advocated by David Harel, as exemplified in some of his books and in his 2013 talk at TU/e, which I attended.
While studying the history of ideas in computer science, I also started to notice that philosophers like James Moore, James Fetzer, and Timothy Colburn, along with the sociologist Donald MacKenzie, had made similar observations years and even decades before me. But computer scientists have mostly ignored these writings, or, as in the case of Fetzer, have ridiculed him. I am of course referring to Fetzer's 1988 article in the Communications of the ACM, entitled: Program Verification: The Very Idea [2]. The story is told in MacKenzie's 2004 book Mechanizing Proof and it should in my opinion be mandatory reading material for students and academics alike.
I, too, was a hard-core formal methodist during my Ph.D. years. Interestingly, none of my peers ever told me that the papers I was reading (i.e., the papers of Edsger Dijkstra, Tony Hoare, and others) were flawed in some, yet crucial, respects — as Fetzer already remarked in 1988. My educated guess is that even top computer scientists are not well aware about the history of their own discipline.
To be even more provocative, chances are that you are a computer scientist who thinks that everybody can and will give the same answer to the following simple, yet fundamental, question:
What is a program?
But wait a minute. Dijkstra says in 1973 that a program is a mathematical object of finite capacity while Christropher Strachey says, in that very same year, that a program is a mathematical object of infinite size. How can that be? Perhaps computer science is not so clear-cut after all. Moreover, Peter Naur insisted that a program is a model of the real world, which is not a logico-mathematical construction. So here we already have three conflicting views on computer science's most basic question.
Subsequent blog posts will shed more light on category mistakes made in computer science, what they are, and which writings of prominent computer scientists I am referring to. In this regard let me also mention the following writings:
- E.G. Daylight. Category Mistakes in Computer Science at Large. Peer reviewed by anonymous referees from POPL in 2015, by the CACM in 2016, and in revised form by POPL in 2016. The POPL referees consider the contents trivial and well known (but see my subsequent blog posts!) while the CACM reviewers fundamentally disagree with my research findings. As a result, I re-wrote a small part of that paper with the philosopher of computer science Giuseppe Primiero, resulting in
- Category Mistakes in Computer Science. Currently under peer review for the CACM.
- Subsequent blog posts will show that programming language experts do at times fuse categories and that conceptual clarity is much in order.
- Moreover, I am currently re-writing the whole text in collaboration with Maarten Bullynck and Liesbeth De Mol, i.e., fellow historians and philosophers of science & technology. Dissemination in a reputable journal of philosophy is feasible but our grand challenge is to successfully reach out to computer scientists.
- Finally, my findings will also appear in 2017 (potentially as part of my forthcoming dissertation on the history & philosophy of computer science).
References
[1] E.G. Daylight, A. Vandecappelle, F. Catthoor. The formalism underlying EASYMAP. Science of Computer Programming, 72(3):71-135, 2008.
[2] J.H. Fetzer. Program Verification: The Very Idea. Commun. ACM 31(9): 1048-1063, 1988.
3 Comments
Fetzer and finiteness
Submitted by CharlieMartin (not verified) on
I had a long argument with Jim Fetzer at the time of the publication of "The Very Idea"; he'd made a basic mistake of his own, which was that he'd explored the literature starting from Dijkstra's and Hoare's seminal papers and books. Unfortunately, at the time references from Eindhoven and Oxford formed a (near-) clique, so Jim never found his way to, for example, Good, Boyer, and Moore at UT Austin, in which his points were rather exhaustively covered. (I was also working as a student intern at Computational Logic at the time, so I was much more aware of them.)
In any case, there is the point specifically that one of the issues involved is undecidability. But if you read Discipline of Programming closely, you'll find that as he first describes the state of a program axoimatically as being the Cartesian product of a finite number of values, each of which was composed of a finite collection of symbols. Thus, necessarily, the state space of a program expressed in the EWD-language was inherently finite-state; halting and equivalence, then, reduce simply to applications of basic theorems about finite state machines.
Boyer & Moore
Submitted by egdaylight on
Thanks! Yes, Dijkstra was all about decidability. Donald MacKenzie's extensive coverage connects Fetzer's 1988 work to that of Boyer, Moore, and others.
Dijkstra and 100% correctness (1993)
Submitted by egdaylight on
I'm currently researching the `James Fetzer controversy' in more detail and, specifically, Dijkstra's developing thoughts on program correctness. In this regard I have also come across a panel debate between Dijkstra and DeMillo at Purdue University on April 16, 1993.
To cut to the chase: I feel a bit uncomfortable about my remark on Dijkstra in this post. My present conjecture is that, trained initially as a theoretical physicist, Dijkstra was very well aware of the categorical distinction between the real world on the one hand and his program as a model (of part of that real world). ..... There is so much more to be said .... and there is absolutely no reason to assume that Dijkstra and Hoare had very similar views on this topic. (Fetzer scrutinizes statements made by Hoare, not by Dijkstra, even though he refers to the writings of both computer scientists.)
By 1993 Dijkstra had already repeatedly distinguished between the Pleasantness Problem on the one hand and the Correctness Problem on the other hand (see some of my previous blog posts on this topic, not to mention my latest book (to be announced very soon)). And even with regard to solely the "scientific" Correctness Problem, Dijkstra did *not* want to put himself in a position where he would have to defend the claim that the program could be made 100% correct (with respect to the given formal specification). In his words from that 1993 debate: "no wise mathematician makes claims to infallibility. He leaves that claim to experts in that field like the pope." It is a recurring theme in the Purdue debate ....
Definitely to be continued ..... Yes, I'm looking forward to getting back to Dijkstra's life and career; that is, to mostly writing historiographical accounts as I tried to do in between 2011 and 2013.