Tony Hoare spoke yesterday at the Computing in the 21st Century Conference in Beijing. Tony is a Turing award winner, Quicksort inventor, author of the influential Communication Sequential Processes (CSP) formal language, and long time advocate of program verification and tools to help produce reliable software systems. In his talk he argues that programming should be and can be a science and the goals should be correct programs that stay correct through change. Zero defect software.
He explains that engineers will accept that there will be defects but the scientist should pursue perfection far beyond that for which there is a commercial need. Tony has spent a big part of his successful career in pursuit of techniques and tools to produce reliable complex systems.
Tony ended his talk on an a practical engineering note hoping that we can advance our field to the point that “Software will contain no more errors than other engineering disciplines”. We’re not there yet.
My rough notes from the talk follow.
Title: The Science of Programming
Speaker: Tony Hoare
The Vision:
· Computer software contains no more errors
o Software is the most reliable component of any device that contains it
· Programmers make no mistakes
o Programs work the first time they run
o They run forever after, even after changing
· Programming is an engineering discipline
o Respected for its delivered benefits and it’s foundation on basic science
· Semantics is the science of programming
o Explores the meaning of computer programs
o Operational: correctness of implementation
o Algebraic: Correctness of optimization
o Axiomatic
The Insight:
· Computer programs are mathematical formulae
o They don’t suffer from rust, wear, decay, fatigue
o If a correct program is started in a correct state, they it will stay correct
· Their correctness is a mathematical conjecture
o To be proved by logic and calculation
o Checked by the computer itself
History of the idea:
· Aristotle (350bc): Syllogistic logic
· Euclid (300bc): geometry
· Leibnitz (1700): calculus
· Boole (1850): laws of thought
· Frege (1880): predicate logic
· Russel (1920): Principia
· Hao Wang (1956): Computer checks
Basic Science:
· Answers fundamental questions
· What does it do?
· How does it work?
· Why does it work?
· How do we know?
What does it do?
· Answered by its behavioral specification
How does it work?
· Answer by it’s internal interface contracts
Why does the program work?
· Answered by programming theory
How do we know?
· By logical/mathematical proof
Ideals in Basic Science
· Pursued for the sake of scientific glory far in advance of commercial need
· Physics: accuracy of measurement
· Chemistry: purity of materials
· Computing Science: zero defect programs
Unifying Theory
· Basic science seeks unifying theories
· Explains diverse phenomena
· Supported by evidence
Overall, industry is not heavily using software verification along the lines that Tony wants to see but there are some in use. For example, some tools in use at Microsoft:
· PREfix and PREfast
· Static Driver Verifier
· ESP (locates potential buffer overflows)
The Hope:
· Software will contain no more errors than other engineering disciplines.
James Hamilton, Data Center Futures
Bldg 99/2428, One Microsoft Way, Redmond, Washington, 98052
W:+1(425)703-9972 | C:+1(206)910-4692 | H:+1(206)201-1859 | JamesRH@microsoft.com
H:mvdirona.com | W:research.microsoft.com/~jamesrh | blog:http://perspectives.mvdirona.com