Lovelace lecture 2011

Making program logics intelligible

Speaker: John Reynolds, professor at the Carnegie Mellon University, Pittsburgh.

To verify program specifications, rather than generic safety properties, it will be necessary to integrate verification into the process of programming. Program proving is unlike theorem proving in mathematics; mathematical conjectures may give no hint as to how they might be proved, but programs are written by programmers who must understand informally why their programs work.

The job of verification is not to explore some immense search space but to formalise the programmer's intuitions until any faults are revealed. This requires specifications and proofs that are succinct and intelligible, which in turn require logics that go beyond predicate calculus (the assembly language of program proving).

In this talk, John Reynolds recounts and illustrates several steps, old and new, towards this goal, including interval and partition diagrams, lacy arrays and separation logic.