**The 2011 lecture was delivered by Professor John Reynolds, Carnegie Mellon University, Pittsburgh, PA.**

### Synopsis

**'Making Program Logics Intelligible'**

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 could 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 formalize 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 recounted and illustrated several steps, old and new, towards this goal, including interval and partition diagrams, lacy arrays, and separation logic.