The Computer Journal presents: The Ideal of Program Correctness by Tony Hoare.

The lecture took place on Wednesday 25th October 2006 and was followed by a debate.

The Talk

Tony Hoare proposed that program correctness is a basic scientific ideal for Computer Science, and should be pursued for its own sake.

In that way, one can accumulate a body of relevant scientific theory, supported by widely ranging experiment, and implemented in an integrated programming toolset to be used by the professional programmer.

Draft paper (56 kb)

The Speaker

Professor Sir Tony Hoare studied Philosophy, Latin, and Greek at Oxford University in the early fifties, Russian during his National Service in the Royal Navy, and the machine translation of languages as a graduate student at Moscow State University (together with probability theory, in the school of Kolmogorov). One outcome of the latter work was the discovery of the Quicksort algorithm.

On returning to England in 1960, he worked as a programmer for Elliott Brothers, and led a team in the development of the first commercial compiler for the programming language Algol 60.

In 1968, he took up a Chair in Computing Science at the Queen's University, Belfast. There his output included a series of papers on the use of assertions in program proving.

In 1977, he moved to Oxford University, where 'provable correctness' was again a focus of his research. Well-known results of this work included the Z specification language, and the CSP concurrent-programming model.

Recently, he has been investigating the unification of a diverse range of theories that apply to different programming languages, paradigms, and implementation technologies.

Throughout his academic career, Tony Hoare has maintained strong contacts with industry, through consultancy, teaching, and collaborative research projects. He has taken a recent interest in legacy systems, where assertions can play an important role in system testing.

In 1999, on reaching retirement age at Oxford, Tony moved back to industry as a Senior Researcher with Microsoft Research in Cambridge, England. In March 2000, he received a knighthood from the Queen for services to Computing Science.

The Discussion

Chair: Nigel Shadbolt (Southampton University). Following Tony Hoare's presentation, a discussion from Mark Josephs (South Bank University) and Cliff Jones (Newcastle University), the debate was extended to the 80-odd participation. Issues raised include the following:

Question: How is a programmer verifier verified? What proportion of programmers could write specifications rather than program code?

Answer: Some people are good at abstraction and some at specification.

Question: End-user programming versus interaction with users - where are formal methods based?

Answer: Different application areas lend themselves to different systems. Computer science education is regrettably often analogous to teaching 'engineering' to all engineering disciplines. Requirements have to be distinguished from correctness.

Question: What are the best formal methods and techniques?

Answer: In fact, there are situations where you should not bother with specification, such as for one-off use. 

Question: How feasible in reality is the verifying compiler?

Answer: It is there in embryo, and the work of Praxis should be looked at. There is still work to be done. 

Question: Are planned tools automatic, and are there significant missing aspects? 

Answer: Tools are and should be as automatic as possible. The Praxis tool states that 84% verification is possible. The problem today, it is suggested, is scaling. And tendentiously, we are targeting fewer programmers, with all that that implies!

Question: Human factors are important,  not just developers and users. Consider the Challenger disaster. So, surely we should address not just programs but systems?  

Answer: Cliff mentioned that Tony has been criticized as addressing closed systems only. Tony's response was to view that as praise!

Question: Will we ever have the verifying  compiler? Is this a feasible Grand Challenge? 

Answer: There are various tools. Real work will blossom at the end of their development, cf. the history of the Human Genome Project. 

Question: How can roles of verification be coordinated? 

Answer: The challenge of a Grand Challenge will lead in itself to greater maturity; cf. how work is focused and channelled with the Large Hadron Collider, or large astronomy facilities.

Question: Again on the formal versus informal spectrum of requirements: do we have to live with less than 100% goals? 

Answer: Yes, we do!

Question: Can we address the problem of correctness by characterizing one program as better than another, as opposed to adherence to specifications? 

Answer: Good science is the goal.

Question: Why are software verification tools not used as widely as for example in chip design?

Answer: Pragmatism is necessary. Prototyping is good too. We need bridges between the formal and the informal. 

Question: Is open source important? Tony's answer: Yes, very.

The paper and the discussion from this lecture was published in the Computer Journal.

Computer Journal Lectures
The Computer Journal