Laws of Programming with Concurrency

The basic Laws of Nature sought by many branches of science, as well as the basic axioms postulated in many branches of mathematics, have historically been expressed in great generality as algebraic equations, or occasionally as inequalities. Nowadays these equations provide the theoretical foundation for the design of automated tools which are widely used to help scientists and engineers in pursuit of their goals. This is the way in which Isaac Newton still contributes to mechanics, Blaise Pascal to statistics, Clark Maxwell to electronics, and George Boole to computer Logic Design. How many Computer Scientists and Software Engineers are familiar with the laws which underlie their own professional practice? They are remarkably similar to the laws of arithmetic, taught even today to schoolchildren. I will present arguments that they are both generally true of computer programs, and provide the foundation for tools that are widely used in programming practice. And the laws of concurrent programming are no more complicated than those for sequential programming.

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.

Date:
Speakers:
Tony Hoare