Philosophy of Computer Science
Can Programs Be Verified?
Last Update: 12 April 2007
Note:
or
material is highlighted

This is an archival version. The latest version is located at:
http://www.cse.buffalo.edu/~rapaport/584/canprogsbeverified.html
"I hold the opinion that the construction of computer programs is a
mathematical activity like the solution of differential equations,
that programs can be derived from their specifications through
mathematical insight, calculation, and proof, using algebraic laws
as simple and elegant as those of elementary arithmetic."
"Computer programming is an exact science in that all the properties of
a program and all the consequences of executing it in any given
environment can, in principle, be found out from the text of the
program itself by means of purely deductive reasoning."
"When the correctness of a program, its compiler, and the hardware
of the computer have all been established with mathematical
certainty, it will be possible to place great reliance on the
results of the program, and predict their properties with a
confidence limited only by the reliability of the
electronics."—C.A.R. Hoare

McCarthy, John (1963), "Towards a Mathematical Science of
Computation", in C.M. Popplewell (ed.), Information Processing
1962: Proceedings of DFIP Congress 62 (Amsterdam:
NorthHolland): 2128; reprinted
in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 3556.

Naur, Peter (1966), "Proof of Algorithms by General Snapshots",
BIT 6: 310316; reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 5764.

Floyd, Robert W. (1967), "Assigning Meanings to Programs", in
Mathematical Aspects of Computer Science: Proceedings of Symposia in
Applied Mathematics, Vol. 19 (American Mathematical Society): 1932;
reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 6581.

Hoare, C.A.R. (1969), "An Axiomatic Basis for Computer
Programming", Communications of the ACM 12: 576580, 583;
reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 8396.

Dijkstra, Edsgar W.
(1974),
"Programming as a Discipline of Mathematical Nature",
American Mathematical Monthly
(JuneJuly): 608612.

Dijkstra, Edsgar W.
(1975),
"Guarded
Commands, Nondeterminacy and Formal Derivation of Programs",
Communications of the ACM 18(8): 453457

De Millo, Richard A.; Lipton, Richard J.; & Perlis, Alan J. (1979),
"Social
Processes and Proofs of Theorems and Programs",
Communications of the ACM 22(5): 271280; reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 297319.
 Naur, Peter (1982), "Formalization in Program Development",
BIT 22: 437453; reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 191210.
 Dijkstra, Edsger W. (1983),
"Fruits of Misunderstanding" (EWD854),
reprinted in Datamation (15 February 1985): 8687.
 Scherlis, William L.; & Scott, Dana S. (1983), "First Steps towards
Inferential Programming", in R.E.A. Mason (ed.), Information
Processing 83 (JFIP and Elsevier Science Publishers): 199212;
reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 99133.
 Olson, Steve (1984, January/February), "Sage of Software",
Science: 7580.

Gries, David (1981),
The
Science of Programming (New York:
SpringerVerlag).
 Meyer, Bertrand (1985), "On Formalism in Specifications", IEEE
Software 2(1) (January): 626; reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 155189.

Smith, Brian Cantwell (1985),
"Limits
of Correctness in Computers" [PDF],
Technical Report CSLI8536 (Stanford, CA: Center for the Study
of Language and Information);
first published
in Charles Dunlop & Rob Kling (eds.), Computerization and
Controversy
(San Diego: Academic Press, 1991): 632646; reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 275293.

Also see:
Fetzer, James H. (1999),
"The
Role of Models in Computer Science" [PDF],
The Monist
82(1):
2036.

Also possibly of relevance:
Jackson, Michael (2003),
"Why Software Writing Is Difficult and Will Remain So" [PDF],
Information Processing Letters
88: 1325.

For more examples like Smith's moonmistakenasmissile,
only with more dire consequences, see:
Neumann, Peter G. (1993),
"Modeling and Simulation",
Communications of the ACM
36(4) (June): 124.

Another interesting article on computational modeling (and
what can go wrong):
Hayes, Brian (2007),
"Calculating the Weather",
American Scientist 95(3) (MayJune): 271273.

On the nature of abstraction, see:

Rapaport, William J. (1999),
"Implementation Is Semantic Interpretation" [PDF],
The Monist
82(1):
109130.

Kramer, Jeff (2007),
"Is Abstraction the Key to Computing?",
Communications of the ACM
50(4) (April): 3642.
 Verity, John W. (1985), "Bridging the Software Gap", Datamation
(15 February): 84, 88.
 Hoare, C.A.R. (1986), "Mathematics of Programming", Byte
(August); reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 135154.
 Floyd, Christiane (1987), "Outline of a Paradigm Change in Software
Engineering", in G. Bjerknes et al. (eds.), Computers and
Democracy: A Scandinavian Challenge (Brookfield, VT: Gower
Publishing): 191210; reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 239259.

Fetzer, James H. (1988),
"Program Verification: The Very Idea",
Communications of the ACM 31(9) (September): 10481063;
reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 321358.
 Ardis, Mark; Basili, Victor; Gerhart, Susan; Good, Donald; Gries,
David; Kemmerer, Richard; Leveson, Nancy; Musser, David; Neumann,
Peter; & von Henke, Friedrich (1989),
"Editorial
Process
Verification" (letter to the editor, with replies by James H. Fetzer
and Peter J. Denning), ACM Forum, Communications of the ACM
32(3) (March): 287290.
 Pleasant, James C.; AND Paulson, Lawrence; Cohen, Avra; & Gordon,
Michael; AND Bevier, William R.; Smith, Michael K.; & Young, William
D.; AND Clune, Thomas R.; AND Savitzky, Stephen (1989),
"The Very
Idea" (5 letters to the editor), Technical Correspondence, Communications of the ACM 32(3) (March): 374377.
 Fetzer, James H. (1989),
"Program
Verification Reprise: The Author's
Response" (to the above 5 letters), Technical Correspondence, Communications of the ACM 32(3) (March): 377381.
 Dobson, John; & Randell, Brian (1989),
"Program Verification: Public
Image and Private Reality", Communications of the ACM 32(4)
(April): 420422.
 Müller, Harald M.; AND Holt, Christopher M.; AND Watters, Aaron
(1989),
"More on the Very Idea" (3 letters to the editor, with reply
by James H. Fetzer), Technical Correspondence, Communications of the ACM 32(4) (April): 506512.
 Hill, Richard; AND Conte, Paul T.; AND Parsons, Thomas W.; AND Nelson,
David A. (1989),
"More on Verification" (4 letters to the editor),
ACM Forum, Communications of the ACM 32(7) (July): 790792.
 Tompkins, Howard E. (1989),
"Verifying FeatureBugs" (letter to the
editor), Technical Correspondence, Communications of the ACM 32:
11301131.

Note: This does not seem to be available online.

Barwise, Jon (1989),
"Mathematical
Proofs of Computer System Correctness" [PDF],
Notices of the American Mathematical Society
36: 844851.
Included in the online version of the above:
 Dudley, Richard (1990), "Program Verification" (letter to Jon Barwise
(ed.), Computers and Mathematics column, with a reply by Barwise), Notices of the American Mathematical Society 37: 123124.
 Blum, Bruce I. (1989), "Formalism and Prototyping in the Software
Process", Information and Decision Technologies 15: 327341;
reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 213238.
 Cohen, Avra (1989), "The Notion of Proof in Hardware Verification",
Journal of Automated Reasoning 5: 127139; reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 359374.
 Colburn, Timothy R. (1991), "Program Verification, Defeasible
Reasoning, and Two Views of Computer Science", Minds and
Machines 1: 97116; reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 375399.
 Fetzer, James H. (1991), "Philosophical Aspects of Program
Verification", Minds and Machines 1: 197216; reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 403427.
 Devlin, Keith (1992), "Computers and Mathematics", Notices of the
American Mathematical Society 39: 10651066.
 MacKenzie, Donald (1992), "Computers, Formal Proofs, and the Law
Courts", Notices of the
American Mathematical Society 39: 10661069.
 Naur, Peter (1992), "The Place of Strictly Defined Notation in Human
Insight", in Computing: A Human Activity (AddisonWesley);
reprinted in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers, 1993): 261274.
 Nelson, David A. (1992), "Deductive Program Verification (A
Practitioner's Commentary)", Minds and Machines 2: 283307.
 Colburn, Timothy R. (1993), "Computer Science and Philosophy", in
Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers): 331.
 Colburn, Timothy R.; Fetzer, James H.; & Rankin, Terry L. (eds.)
(1993), Program Verification: Fundamental Issues in Computer Science
(Dordrecht, Holland: Kluwer Academic Publishers).
 contains a lengthy bibliography
 Nelson, David A. (1993), Review of Boyer & Moore's A
Computational Logic Handbook and Moore's Special Issue on System
Verification (Journal of Automated Reasoning), in Minds and
Machines 4: 93101.
 Fetzer, James H. (1993), "Program Verification", in Allen Kent &
James G. Williams
(eds.),
Encyclopedia of Computer Science and
Technology, Vol. 28, Supp. 13 (New York: Marcel Dekker): 237254;
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): 4764.
 Bowen, J.P., & Hinchey, M.G. (1995), "Ten Commandments of Formal Methods",
IEEE Computer 28(4): 5663.
 Glanz, James (1995), "Mathematical Logic Flushes Out the Bugs in Chip
Designs", Science 267: 332333.

Fetzer, James H. (1998),
"Philosophy and Computer Science:
Reflections on the Program Verification Debate", in
Bynum, Terrell Ward; & Moor, James H. (eds.),
The Digital Phoenix:
How Computers Are Changing Philosophy, Revised Edition
(Oxford: Blackwell): 253273.
 Fetzer, James H. (1996), "Computer Reliability and Public Policy:
Limits of Knowledge of ComputerBased Systems", Social Philosophy
and Policy, forthcoming.

Neumann, Peter (1996, July),
"Using
Formal Methods to Reduce Risks",
Communications of the ACM
39(7): 114.
 Pollack, Andrew (1999, May 3), "For Coders, a Code of Conduct: 2000 Problem
Tests Professionalism of Programmers", The New York Times: C1, C12.
Copyright © 20042007 by
William J. Rapaport
(rapaport@buffalo.edu)
http://www.cse.buffalo.edu/584/S07/canprogsbeverified.html20070412