Abstract

It’s nice when somebody tells you about their uncle. Especially when they start out telling you about their father’s farm and then all of a sudden get more interested in their uncle. I mean it’s dirty to keep yelling “Digression!” at him when he’s all nice and excited. I don’t know. It’s hard to explain… (from The Catcher in the Rye, by J. D. Salinger)

I will present an example and presentation slides from a recent keynote by J Strother Moore at the 2011 Conference on Formal Methods in Computer Aided Design (FMCAD 2011). The talk title is, “The Role of Human Creativity in Mechanized Verification.” The example is a running account of an classroom “proof discovery” exercise. It illustrates how the most meaningful aspects of reasoning—from the perspective of the formal methods researcher—are lost by the time the goal is achieved. Of course, we all know this. We are told never to dwell on the blind alleys we’ve followed. Moore argues just the opposite; the blind alleys are of the essence to one building tools for reasoning.

Moores presentation, is included in the FMCAD 2011 procedings at www.cs.utexas.edu/~hunt/FMCAD/FMCAD11/advance-program.html