Jean Yang on An Axiomatic Basis for Computer Programming

Jean Yang explains Tony Hoare's seminal 1969 paper on Hoare logic and the axiomatic basis for computer programming.

Meetup: meetup.com/papers-we-love/events/214400572/ Paper: cs.cmu.edu/~crary/819-f09/Hoare69.pdf Slides: speakerdeck.com/paperswelove/jean-yang-on-an-axiomatic-basis… Audio: mixcloud.com/paperswelove/jean-yang-on-an-axiomatic-basis-fo… --------------------------------------------------------------------------------------------- Sponsored by The Ladders (@TheLaddersDev) --------------------------------------------------------------------------------------------- Description --------------- Our lives now run on software. Bugs are becoming not just annoyances for software developers, but sources of potentially catastrophic failures. A careless programmer mistake could leak our social security numbers or crash our cars. While testing provides some assurance, it is difficult to test all possibilities in complex systems--and practically impossible in concurrent systems. For the critical systems in our lives, we should demand mathematical guarantees that the software behaves the way the programmer expected. A single paper influenced much of the work towards providing these mathematical guarantees. C.A.R. Hoare’s seminal 1969 paper “An Axiomatic Basis for Computer Programming” introduces a method of reasoning about program correctness now known as Hoare logic. In this paper, Hoare provides a technique that 1) allows programmers to express program properties and 2) allows these properties to be automatically checked. These ideas have influenced decades of research in automated reasoning about software correctness. In this talk, I will describe the main ideas in Hoare logic, as well as the impact of these ideas. I will talk about my personal experience using Hoare logic to verify memory guarantees in an operating system. I will also discuss takeaway lessons for working programmers. Bio ---- Jean Yang (@jeanqasaur) is a final-year PhD student at MIT. For her PhD thesis she has created Jeeves, a programming language for automatically enforcing information flow policies for security and privacy. You may be more familiar with one of her other projects, Haskell Ryan Gosling.