Readings

R020100c: The Road to Trustworthy Computing

Donald McKenzie has provided a time-line for the development of ideas around trust and proof in computing [MacKenzie1998: Appendix].

These notes build on the McKenzie time-line to form a chronology for trustworthy computing.

Last updated 2002-02-03-17:44 -0800 (pdt)

The Beginnings

Here we might consider the activities in the 19th and early 20th century, culminating in the work of Gödel and Turing.  The chronology in Advent of the Algorithm might be appropriate here.

1950 Digital Optimism

I am using decades as arbitrary boundaries, though there are enough interesting patterns to practically claim a fit.

1955/56 Newell, Shaw, Simon: Logic Theory Machine

1959 Herbert Gelernter: Geometry Machine

1960

1960 Hao Wang champions algorithmic against heuristic theorem provers

1962 John McCarthy: "Towards a Mathematical Science of Computation"

1963 Alan Robinson: Resolution, a machine-oriented inference rule

1966 Peter Naur: "Proof of Algorithms by General Snapshots"

1967 R.W. Floyd: "Assigning Meanings to Programs"

1967 First public discussion of computer security vulnerabilities of US defence systems

1968 NATO conference on Software Engineering at Garmisch: diagnosis of "software crisis"

1969 C. A. R. Hoare: "An Axiomatic Basis for Computer Programming"

1970

1971 Robert Boyer and J. Strother Moore begin collaboration that leads to their theorem prover

1973-80 SRI PSOS project. Provably Secure Operating System

1976 Appel and Haken prove four-colour conjecture, using 1200 hours computer time

1978-87 SRI proof work on SIFT fault-tolerant avionics computer

1979 DeMillo, Lipton and Perlis attack program proof in Communications of the ACM

1980

1983 "Orange Book." Design proof required for A1 secure systems

1983 SIFT Peer Review

1984-85 VIPER proof effort begins at Royal Signals and Radar Establishment

1985 Honeywell Secure Communications Processor: first system to achieve A1 rating.

1986-90 Disputes over Trip Computer Software delay licensing of Darlington, Ontario, nuclear power station

1986 First clear-cut software error deaths: overdoses from Therac-25 radiation therapy machines

1987 Inmos T800 transputer: floating-point unit microcode formally verified

1987-88 Commercialisation of VIPER begins

1988-89 Entry into service of Airbus A320, first fly-by-wire airliner

1988 Crash of A320 at Habsheim air show triggers fierce controversy in France

1988 James Fetzer attacks program proof in Communications of the ACM

1989 Formally verified SACEM train protection software enters service on RER, Paris

1990

1991 UK Interim Defence Standard 00-55: proof required for systems most critical to safety

1991 VIPER law suit

1994 Hackers seize control of computer network at USAF Rome (N.Y.) Lab

1994 Pentium divide bug

1995 Entry into service of Boeing 777, most computer-intensive airliner to date

1996 New computer-assisted proof of four-colour theorem by Robertson et al.

2000

References

[Berlinski2000]

Berlinski, David.  The Advent of the Algorithm: The Idea That Rules the World.  Harcourt (New York: 2000).  ISBN 0-15-100338-6.
 

[MacKenzie1998]

MacKenzie, Donald A.  Computers and the Sociology of Mathematical Proof.  Prepared for Northern Formal Methods Workshop, Ilkley, September 1998.  Edinburgh University Department of Sociology.  Published on-line.
 

[MacKenzie2001]

MacKenzie, Donald A.  Mechanizing Proof: Computing, Risk, and Trust.  MIT Press (Cambridge, MA: 2001).  Inside Technology Series.  ISBN 0-262-13393-8 hard cover, alkaline paper.

created 2002-02-02-23:23 -0800 (pst) by orcmid
$$Author: Orcmid $
$$Date: 02-10-13 13:22 $
$$Revision: 6 $