A: The challenge of construction of a routinely usable Program Verifier was first proposed in 1969 by Jim King in his Doctoral Dissertation. Since that time, the power and capacity and sheer numbers of installed computers have each increased more than a thousand-fold; and a thousand-fold advance has been made in certain aspects of mechanised theorem proving (e.g., SAT solving). There have been useful conceptual advances in programming theory, and there is already useful experience of construction of manual proofs for critical programs. The cost of programming error to the economy of the world has similarly escalated.

If all the advances in software and hardware technology can be brought to bear in a coordinated project for the delivery of a program verifier, the prospect of success is much greater than it ever has been in the past. Even though the risks are still high, this is the kind of challenge that must be attempted again; because the potential of reward far outweighs the risk. Even in the event of failure, some beneficial spin-off is likely; and another attempt will surely be made later.

Q2. It has been over 35 years since the publication of the classic paper, An Axiomatic Basis of Computer Programming, by Tony Hoare. Yet, very few schools teach formal methods in U.S.A. and most practitioners avoid any formal work. What do you expect it will take to effect a paradigm shift?

A: The existence (or even the near prospect) of an automatic program verifier may well be the trigger for the necessary paradigm shift. It may break the vicious circle of students who do not wish to learn a technology that is not used in industry, and an industry that is reluctant to apply a technology in which their recruits are not trained.

The crucial motivation for education in the principles of verification is that it is driven by scientific ideals, in that it addresses the questions fundamental in all branches of engineering science. For any product of engineering, the qualified engineer must be able to answer questions on what it does and how it works. Scientists should be able to answer deeper questions, explaining why it works, and how we know that the answers to the previous questions are correct. Even if the fundamental achievements of pure science seem remote from practical application, good engineers and entrepreneurs eventually find ways of exploiting established scientific theories and tools.

Q3. How will you educate managers, software designers and programmers for this paradigm shift?

A: There is good evidence that intellectually live programmers can be educated in the principles and practice of specification and verification. For example, the Department of Continuing Education at Oxford runs a part-time Professional Development Masters Degree, which attracts many students from the British software Industry. The United Nations University in Macau has concentrated their research and education on formal methods of software engineering. Their experience is available to be exploited and generalised in the development of tools and texts for general education.

Q4: How would you train verification engineers? Should they have domain knowledge, say in banking or medical profession? What kind of CS background should they have? How long should they be trained?

A: The patterns for professional education in other branches of Engineering should be followed as closely as possible. A good general engineering education is a mixture of mathematics, general science and general engineering. It is illustrated by more detailed studies and exercises in a particular domain of application. But good engineers will always look forward to mastering or at least understanding many other specialisations, as the need arises during their professional career.

Q39: Is this challenge grand enough? Would it possibly suck money away from other worthy projects where advances in basic sciences can be made?

A: The initiation of a good scientific challenge should not be dependent on any significant increase of funding. We could recommend this project as just one of the more efficient ways of way of spending whatever money is allocated for the advancement of Computer Science. Because Science is cumulative, progress can be made, albeit more slowly, even with the same absolute amounts of funding, provided the funds are distributed wisely.

Because of the risks, we think it would be dangerous if this project absorbed more than a few percent of the total world-wide expenditure on research in Computer Science. Verification only solves one of the problems of effective computer application, and continued research support is essential in all the other areas relevant to the delivery of dependable and useful software.