Tuesday, June 28, 2016
Speaker: Tony Hoare
Venue: IST Austria
CS Talk series
A theory of programming has many presentations, each suited for a particular purpose. (1) A model defines the details of the traces of execution of a program, in a form useful for discovering, locating and correcting program errors. (2) An algebra gives laws as equations and inequalities between programs. It defines the valid optimisations to which a program may be subjected. (3) A logic gives a method of establishing correctness of programs in terms of preconditions and postconditions. It is used in program analysers checkers to find which parts of a program are free from certain generic errors. (4) An operational semantics describes the individual steps in the execution of the program in terms of the state before and after each step. It is used in the design of compilers and interpreters for a programming language.
A Unified Theory is one that establishes the mutual consistency of these four presentations. I give a simple example how this is done, concentrating primarily on features of concurrency and distribution. The model is simpler than school geometry, the laws are simpler than school algebra, the logic uses Hoare triples, and the semantics uses Milner transitions. It is hoped that the general audience will have some recollection of some of these ideas.
Tony Hoare has a first degree in classical languages, literature, history and philosophy. He has professional qualifications as a Statistician and as a Russian Interpreter. But his primary interest is in Philosophy, which he has sought to apply to computer programming languages throughout his fifty year academic and industrial career.