Philosophy of Computer Science: Online Resources

Further Readings for Chapter 15:

Computer Programs as Mathematical Objects

Note 1: Many of these items are online; links are given where they are known. Other items may also be online; an internet search should help you find them.

Note 2: In general, works are listed in chronological order. (This makes it easier to follow the historical development of ideas.)

§15.1.1: Bugs and Intended Behavior:

• On bugs:
  • On the history of the term 'bug', see:
    • Hopper, G.M. (1981). The first bug. Annals of the History of Computing, 3(3):285–286

    • Krebs, A. and Thomas, Jr., R.M. (1981, 7 August). Historic moth. New York Times, page B5

  • The idea that the first computer bug was really a bug (actually, a moth) is an urban legend, because the term was used in the non-entomological sense as early as 1875; see:
    • Shapiro, F.R. (1985, 24 March). Debugging etymologies. New York Times (letter to the editor)

    • The OED entry for 'bug', definition 5

  • For a photo of the allegedly first "bug", see The Jargon File, which traces the term back to Shakespeare!

    

  • For more on bugs, see:
    • Widder, David Gray; & Le Goues, Claire (2024), "What Is a 'Bug'?", Communications of the ACM 67(11) (November):32–34.
    

• On intended behavior:
  "Maybe I made a mistake. But [John] Cage says: A 'mistake' is beside the point. Once anything happens, it authentically is."
  —Richard Powers, Orfeo: A Novel (New York: W.W. Norton, 2014), p. 11.

• For more on miscomputation, see:
  Fresco, Nir; & Primiero, Giuseppe (2013), "Miscomputation", Philosophy & Technology 26:253–272.

§15.1.2: Proofs and Programs:

• Dijskstra 1972, pp. 9–11, has a discussion about the nature and value of formal proofs of "obvious" theorems that is relevant to the issues raised by De Millo et al. 1979 and Rosser's time-traveler.

• Devlin, K. (1992). Computers and mathematics (column). Notices of the American Mathematical Society, 39(9):1065 1066,
  • An introduction to:
    • MacKenzie, D. (1992). Computers, formal proofs, and the law courts. Notices of the American Mathematical Society, 39(9):1066–1069.

  • Contains a dialogue between a math professor who defends De Millo et al 1979's notion of "social" proof and a philosophy student who defends the more formal, logical notion of proof.

• Lipton, R.J. (2019, 21 October). A polemical overreach? Gödel's Lost Letter and P=NP
  • A more recent commentary on De Millo et al 1979 by one of its authors.

• Thurston, W.P. (1994). On proof and progress in mathematics. Bulletin of the American Mathematical Society, 30(2):161–177.
  • An interesting contrast to Suber 1997 on the relationship between computer programs and mathematical proofs.

• Davis, P.J. and Hersh, R. (1998). "The Ideal Mathematician", in their The Mathematical Experience. Houghton Mifflin, Boston, pp. 34–44.
  • A partly facetious description of the behavior of (some) mathematicians, including a discussion of the nature of proof as carried out by mathematicians.
  • For an antidote to their characterization of mathematicians, read:
    • Frenkel, E. (2013). Love and Math: The Heart of Hidden Reality. Basic Books, New York.

§15.3: Program Verification:

• Colburn, T.R., Fetzer, J.H., and Rankin, T.L., editors (1993). Program Verification: Fundamental Issues in Computer Science. Kluwer Academic Publishers, Dordrecht, The Netherlands.
  • An anthology containing many of the papers discussed in this chapter, as well as an extensive bibliography on program verification.

• Colburn himself, some of whose views on the philosophy of CS we have examined in earlier chapters, has two papers on program verification that are worth reading:
  • Colburn, T.R. (1991). Program verification, defeasible reasoning, and two views of computer science. Minds and Machines, 1:97–116.
    • Reprinted in Colburn et al. 1993, pp. 375–399.

  • Colburn, T.R. (1993). Computer science and philosophy. In Colburn et al. 1993, pp. 3–31.

• The origins of program verification can be found in:
  • McCarthy, J. (1963). Towards a mathematical science of computation. In Popplewell, C., editor, Information Processing 1962: Proceedings of the DFIP Congress 62, pages 21–28. North-Holland, Amsterdam.
    • Reprinted in Colburn et al. 1993, pp. 35–56.

  • Naur, P. (1966). Proof of algorithms by general snapshots. BIT, 6:310–316.
    • Reprinted in Colburn et al. 1993, pp. 57–64.

  • Floyd, R.W. (1967). Assigning meanings to programs. In Mathematical Aspects of Computer Science: Proceedings of Symposia in Applied Mathematics, Vol. 19, pages 19‐32. American Mathematical Society.
    • Reprinted in Colburn et al. 1993, pp.–65–81.

  • And, most importantly:
    • Hoare, C.A.R. (1969). An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580, 583.
      • Reprinted in Colburn et al. 1993, pp. 83–96.

    • For Hoare's later views, see:
      • Hoare, C.A.R. (2009). Retrospective: An axiomatic basis for computer programming. Communications of the ACM, 52(10):30–32.

      • Shustek, L. (2009). An interview with C.A.R. Hoare. Communications of the ACM, 52(3):38–41.

• Dijkstra, E.W. (1974). Programming as a discipline of mathematical nature. American Mathematical Monthly, 81(6):608–612.
  • Argues …
    1. … "that the correctness of programs could and should be established by proof",
    2. … that structured programs are simpler to prove than unstructured ones …
       • (On that point, see:
         • Dijkstra, E.W. (1968). Go to statement considered harmful. Communications of the ACM, 11(3):147–148.)

    3. …that theorems about programs make program proofs easier, and (4) that "to prove the correctness of a given program was … putting the cart before the horse. A much more promising approach turned out to be letting correctness proof and program grow hand in hand" (pp. 609–610).

  • See also:
    • Dijkstra, E.W. (1983). Fruits of misunderstanding (EWD-854).
      • Reprinted in Datamation (15 February 1985): 86–87.

• Verity, J.W. (1985). Bridging the software gap. Datamation, pages 84–88.
  • Contains interviews with Dijkstra, Hoare, and Gries.

• Mili, A., Desharnais, J., and Gagné, J.R. (1986). Formal models of stepwise refinement of programs. ACM Computing Surveys, 18(3):231–276, §1.
  • Contains a formal presentation of program correctness.

• These two papers show how to use program-verification techniques to develop programs:
  • Tam, W.C. (1992). Teaching loop invariants to beginners by examples. SIGSCE Bulletin, 24(1):92–96.

  • Arnow, D. (1994). Teaching programming to liberal arts students: Using loop invariants. ACM SIGCSE Bulletin, 26(1):141–144.

• MacKenzie 1992 discusses a legal challenge to a claim that a certain computer program had been verified. The claim was that the verification was of the relatively informal, De Millo et al. 1979-style variety of proof; the challenge was that a formal, mathematical proof was necessary.

• Frenkel, K. (1993). An interview with Robin Milner. Communications of the ACM, 36(1):90–97.
  • Discusses program verification, among other topics.

§15.4: The Fetzer Controversy:

• The following letters to the editor (with replies by Fetzer) are representative of the battle that resulted from Fetzer's article:

  • Pleasant, J.C., Paulson, L., Cohen, A., Gordon, M., Bevier, William R. and Smith, M.K., Young, W.D., Clune, T R., and Savitzky, S. (1989). The very idea (5 letters to the editor). Communications of the ACM, 32(3):374–377.

  • Fetzer, J.H. (1989). Program verification reprise: The author's response [to Pleasant et al. 1989]. Communications of the ACM, 32(3):374–377.

  • Dobson, J. and Randell, B. (1989). Program verification: Public image and private reality. Communications of the ACM, 32(4):420–422.

  • Müller, H.M., Holt, C.M., and Watters, A. (1989). More on the very idea (3 letters to the editor, with reply by J.H. Fetzer). Communications of the ACM, 32(4):506–512.

  • Hill, R., Conte, P.T., Parsons, T.W., and Nelson, D.A. (1989). More on verification (4 letters to the editor). Communications of the ACM, 32(7):790–792.

  • Tompkins, H.E. (1989). Verifying feature-bugs. Communications of the ACM, 32:1130–1131.

• See also:
  • Dudley, R. (1990). Program verification. Notices of the AMS, 37:123–124. Letter to the editor, with reply by J. Barwise.

• For Fetzer's later writings on the controversy, see:

  • Fetzer, J.H. (1991). Philosophical aspects of program verification. Minds and Machines, 1:197–216.
    • Reprinted in Colburn et al. 1993, pp. 403–427
    • A summary, reply to objections, and further discussion of the relation of software to hardware

  • Fetzer, J.H. (1993). Program verification. In Kent, A. and Williams, J.G., editors, Encyclopedia of Computer Science and Technology, Vol. 28, Supp. 13, pages 237–254. Marcel Dekker, New York.
    • Reprinted in Allen Kent & James G. Williams (eds.), Encyclopedia of Microcomputers, Vol. 14: "Productivity and Software Maintenance: A Managerial Perspective to Relative Addressing" (New York: Marcel Dekker): 47–64.
    • An encyclopedia-style article on program verification, from Fetzer's perspective

  • Fetzer, J.H. (1996). Computer reliability and public policy: Limits of knowledge of computer-based systems. Social Philosophy and Policy, 13(2):229–266.
    • "… in the real world, the operation of computer systems is inherently uncertain, which raises profound problems for public policy" (from the Abstract)

  • Fetzer, J.H. (1998). Computer sytems: The uncertainty of their reliability. Bridges, 5(3/4):197–217.
    • "The reliability of computer systems … depends on the … interaction of hardware and software … and the accuracy and completeness of the knowledge upon which they are based. … The reliability of computer-based systems is necessarily uncertain … [and] must not be taken for granted" (from the Abstract).

• MacKenzie, D. (2001). Mechanizing Proof: Computing, Risk, and Trust. MIT Press, Cambridge, MA, Ch. 6, "Social Processes and Category Mistakes".
  • Concerns the De Millo et al.-Fetzer controversy.
  • For a review, see:
    • Hayes, B. (2002, July-August). The search for rigor. American Scientist, 90:382–384.

• Glass, R.L. (2002). The proof of correctness wars. Communications of the ACM, 45(8):19–21.
  • A historical survey, with some useful references, arguing that the controversies over program verification are "extremely healthy for the field" of computing, roughly for the same reasons that (as argued in our book's §2.4) philosophy is important: the challenging of assumptions.

• A point similar to Fetzer's was made by the philosopher and logician Saul Kripke possibly as early as 1974 (when the lecture that Kripke's 2023 paper was based on was first given), in:
  Kripke, Saul A. (2023), "The Question of Logic", Mind:
  "Surely, if a machine set up to do [the logic in Bertand Russell's and Alfred North Whitehead's] Principia Mathematica concludes, let's say, that the distributive law fails in Principia Mathematica's logic, one would think that something has gone wrong with either the programming or with (say) the fuse, not that it doesn't hold in Principia Mathematica. Why? Because if we have this concrete object in front of us, our belief that it produces exactly the same results that would hold in Principia Mathematica depends on (a) a mathematical proof that any abstract Turing machine so programmed will do so (one that uses both logic and mathematics); (b) a physical argument that this particular object, built up in this physical way, will behave like this Turing machine program (that depends on our beliefs in the laws of physics); and (c) an engineering hope that, in fact, the machine is well enough set-up that it won't blow a fuse at this point." (p. 26)

• Long after the Fetzer controversy, articles for and against program verification continue to be published:

  • Neumann, P.G. (1996). Using formal methods to reduce risks. Communications of the ACM, 39(7):114.

  • Henzinger, T. (1996). Some myths about formal verification. ACM Computing Surveys, 28(4es). Article No. 119.
    • Argues in favor of program verification.

  • Tedre 2007, p. 108.
    • Also argues in favor of program verification, but says that "one cannot formally prove either that an engineered product has the intended qualities or that an engineered product will not fail … ".

  • Hinchey, M., Jackson, M., Cousot, P., Cook, B., Bowen, J.P., and Margaria, T. (2008). Software engineering and formal methods. Communications of the ACM, 51(9):54–59.

  • Dewar, R. and Astrachan, O. (2009). CS education in the U.S.: Heading in the wrong direction? Communications of the ACM, 52(7):41–45.
    • A debate over the teaching of formal reasoning in computer science, including program-verification techniques.

  • Leroy, X. (2009). Formal verification of a realistic compiler. Communications of the ACM, 52(7):107–115.
    • See also the introductory editorial:
      • Morrisett, G. (2009). A compiler's story. Communications of the ACM, 52(7):106
      containing philosophical remarks on the value of program verification.

• Lamport, L. (2015). Who builds a house without drawing blueprints? Communications of the ACM, 58(4):38–41.
  • Argues that:
    1. "the main reason for writing a formal spec[ification] is to apply tools to check it",
    2. that "the math needed for most specifications is quite simple: predicate logic and elementary set theory",
    3. that "a specification can and should be embedded as a comment within the code it is specifying",
    4. and — perhaps most importantly — that

       "thinking does not guarantee that you will not make mistakes. But not thinking guarantees that you will."

• Fetzer says (email, 12/19/23), concerning my presentation of his views:
  The sentence at the top of page 359 is not quite right. We must distinguish between computer programs (as implementations of algorithms), which are deductively verifiable; and physical computers that execute them (when they are implemented in computers). The programs as such are abstract, not in space/time, and are amenable to deductive verification.

  The computers used to execute the programs, by contrast, are physical, in space/time, and are only amenable to empirical confirmation. It's a category mistake (a logical blunder) to think we can have the kind of certainty about the performance of a causal system in the world that we can have about an abstract object.

  Simple example: A physical machine in a physical room runs on electricity and will not complete its tasks without it. Even a verified program, uploaded into the machine, cannot guarantee what will happen when the machine executes that program because, for example, there might be a power failure (as you also observe).

  The blunder therefore is to confound abstract objects with causal systems, We can possess deductively certain knowledge about algorithms relating inputs to outputs as abstract entities. But we can only have inductive confirmation for the performance of machines when they execute those programs.

  Hence, the offending sentence, "for Fetzer (and Cleland), computing is about the world; it is external (or "wide"). Thus, computer programs can't be ("absolutely" or "externally") verified, because the world may not be conducive to "correct" behavior:…" where the rest is fine.

  It would be more appropriate to say, "There are abstract computers (which are not in space/time) that are amenable to deductive proofs (that specified inputs yield specified outputs, on the basis of their programs. But they are not the same as physical computers (which are in space/time) that are only open to inductive reasoning, which means that the causal performance of physical computers — even when executing deductively verified programs — cannot be predicted with deductive certainty but only with inductive fallibility."

  To which I responded:
  Would it have been better for me to have said something like this?:
  "…physical computing is about the world… thus, the physically realized execution of a computer program can't be ("absolutely" or "externally") verified…"

  And to which Fetzer replied:

  Sure. Something like that. Not a big deal. I think you get the point across, even if I might have explained it a bit differently. The emphasis should be on abstract objects vs. causal systems, where the former are amenable to deductive proof but the latter only to inductive confirmation. Hence, we can have certain knowledge about the former but only uncertain knowledge about the latter.

§15.6.2: Models: Putting the World into Computers:

• On a map that is the same size as what it maps:
  • The earliest discussion is in:
    • Carroll, Lewis (1893). Sylvie and Bruno Concluded. Macmillan, London. Ch. 11.

    • See also: "Quote of the Day: Lewis Carroll's Paradox of the Complete Map".

  • Other discussions of the idea can be found in:

    • Royce, J. (1900). The World and the Individual. Macmillan, London, pp. 502–507ff.

    • Rosenblueth and Wiener 1945, p. 320.

    • Rapaport, W.J. (1978). Meinongian theories and a Russellian paradox. Noûs, 12(2):153‐180, §5.

    • Borges, J.L. (1981). Partial enchantments of the Quixote. In Monegal, E.R. and Reid, A., editors, Borges, A Reader; A Selection from the Writings of Jorge Luis Borges, pages 232–235. E.P. Dutton, New York, esp. p. 234

    • Eco, U. (1982). On the impossibility of drawing a map of the empire on a scale of 1 to 1. In How to Travel with a Salmon and Other Essays, pages 95–106. Harcourt Brace, New York.

  • All of these concern space, but there is an analogous problem for time:
    • Weather prediction is based on models of the world that have to be "capable of scrolling ahead to the future faster than time can progress" (Fry, H. (2019, 1 July). Looks like rain: How weather forecasting got good. The New Yorker, pages 61–65).

• On what I am calling "Smith's gap" between the model and the world, see:
  • Fetzer, J.H. (1999). The role of models in computer science. The Monist, 82(1):20 36.
    • A clearly written summary and critique of Smith's essay.
    • Argues that there are more than merely the two models that Smith considers (a specification as a model of the world and a program as a model of the specification).

  • Jackson, M. (2003). Why software writing is difficult and will remain so. Information Processing Letters, 88:13–25.
    • Discusses "the interplay between the formal world of the computer and its programming language with the informal world where the problem to be solved is located" (from the abstract, p. 13).

  • van Fraassen, B.C. (2006). Representation: The problem for structuralism. Philosophy of Science, 73:536–547.
    • Discusses the relation between formal, mathematical models of reality and the reality of which they are models, arguing that what I call Smith's gap presents difficulties for scientific realism (§4.5).

  • Rescorla, M. (2015). The representational foundations of computation. Philosophia Mathematica, 23(3):338–366.
    • Identifies "a gap between the domain of items manipulated by the Turing machine and our desired domain of computation" (§1).
    • From the existence of this gap — which seems clearly akin to Smith's — Rescorla argues "that computability theory is an intensional enterprise …: it studies entities as represented in certain ways, rather than entities detached from any means of representing them" (§1).

      • On "intenSionality" with an 's', see our §3.4.2 and
        Rapaport, W.J. (2012). IntenSionality vs. intenTionality.

  • Smith's gap is also related to the issues surrounding attempts to prove the Computability Thesis from axioms that are intended to capture the informal notion of computability (such as Dershowitz and Gurevich 2008 and Sieg 2008):
    "… how [can] we tell whether a given piece of live mathematical reasoning corresponds to a given actual or envisioned formal proof … How does one guarantee that the stated axioms or premises of the formal proof are in fact necessary for the intuitive, pre-theoretic notions invoked in the informal text? That is, how do we assure ourselves that the formalization is faithful? This question cannot be settled by a formal derivation. That would start a regress, at least potentially. We would push our problem to the axioms or premises of that derivation. Moreover, any formalization of a real-life argument reveals missing steps, or gaps, and plugging those would sometimes require theses much like Church's thesis" (Stewart Shapiro 2013, pp. 158–159).