PhD: Can computers understand their own programs?

July 5, 2012
Tony Hoare | MSR Cambridge

In his centenary year, it is appropriate to address a question that interested him. I will suggest that an answer can be found in Turing’s own works.

Turing invented the stored-program digital computer in 1936, with the specific purpose of defining clear limits to the understanding a computer can have of its own programs. He proved that a computer cannot always reliably answer a most important question: Will its own program ever terminate? This impossibility theorem has ever since lain at the foundation of computer science. But let us accept a lower criterion of computer understanding, that allows occasional failure to answer questions.

In 1947, Turing gave a much more positive answer to my question. He showed how a computer could often reason correctly about the correctness of its own programs. My entire research career has been devoted to the development of Turing’s method for reasoning about programs. I now see his method used in the worldwide software industry to reduce the cost of testing programs and the risk of residual program errors in service.

With further research and development, I’m confident that computers will routinely be able to answer a programmer’s general questions about program properties and behaviour. The answers will be useful at all stages of program design, development, and evolution. The collaboration of the programmer with the computer will reveal that the computer understands the details of the program, perhaps not perfectly, but certainly better than the programmer. (But the programmer understands much better the purpose of the program!).

I suggest that Turing would accept this test as a relevant analogue (in the specialised field of software engineering) of his famous Turing test for more general computer intelligence. But one question that remains for philosophical speculation is: Will a computer ever realise that it is reasoning about itself?

Speaker Details

Tony Hoare’s computing interests were stimulated by his first (and only) degree in the humanities (1956): he studied Latin and ancient Greek, followed by philosophy, with particular interest in mathematical philosophy and logic. He learnt Russian during National Service in the Royal Navy. He spent a postgraduate year studying statistics at Oxford and another at Moscow State University, where he discovered the sorting algorithm Quicksort. In 1960, he joined the British Computer industry as a programmer, eventually rising to the rank of Chief Engineer.

His Academic career started in 1968 with appointment as professor at the Queen’s University, Belfast. He chose his long-term research area as proof of the correctness of programs. In the thick of the troubles, he built up a strong computing department, and moved in 1978 to do the same at Oxford. Following the example of Theoretical Physics, his interests broadened to the pursuit of Unifying Theories of Programming.

On reaching retiring age, he accepted an offer of employment at Microsoft Research in Cambridge, where he has seen a strong surge of interest in automation of computer proofs of program correctness. He continues to pursue this interest, while exhorting academic researchers in long-term pursuit of even more idealistic scientific goals.