Oral history of British science
Hoare, Tony (Part 10 of 15). An Oral History of British Science.
The British Library Board acknowledges the intellectual property rights of those named as contributors to this recording and the rights of those not identified.
Legal and ethical usage »
Interviewee’s home, Cambridge
Hoare, Charles Antony Richard, 1934- (speaker, male)
Lean, Thomas (speaker, male)
Part 10: Comments on interest in axiomatic definition of programming languages: benefits of axioms; varied manufacturer specific implementations of computer languages; need for means to describe programming language independent from machine differences; definitions and relevance of axioms and postulates; [06:00] ideal balance of strength of definition of languages; anecdote about TH first introducing formal language definition languages at a conference in Vienna, ideas becoming attractive recently; [08:20] article written at NCC; story about rediscovering a jellygraph of an article by Robert Floyd, usefully suggesting a more direct method for proving program correctness. [11:00] Remarks on 'An axiomatic basis for computer programming': writing paper in Belfast introducing use of Hoare Triples; long lasting importance for TH's academic reputation; disadvantages of method compared to TH's current thinking; notation and execution in high level languages; TH seeing subject as an ideal academic problem due to its long term nature; anecdote about retiring to Microsoft to apply work, growth of computer virus increasing importance of TH's work on program verification. [19:20] Comments on benefits of academic research environment in solving real world problems in the long term, comparisons with lengthy period between Newton's theory on gravity and it's application in World War 1; TH always claiming work was of benefit to industry, benefits of links to industry. [24:00] Description of TH's research process: beginning with writing a paper; paper using proofs of quick sort partition, later application to buffer overflow problems; TH surprised to return to work in industrial research at Microsoft in 1997 at invitation of Roger Needham. [28:40] Remarks on academic career in 1970s: freedom to pursue academic work as he saw fit; pressure caused by need to apply for grants; benefits of links with industry, with example of IBM support; influence of TH's industry career on work on language definitions; TH philosophy of seeking inspiration by pursuing quixotic activities; anecdote about being inspired by questions during recent talks. [34:25] Remarks on: having resources to found a research group at Belfast; PhD student Michael Foley, work with TH on recursive programs, beaten in sectarian attack now a poet.
Interview with computer scientist Sir Tony Hoare.