Memories: doing my PhD at Stanford, under John L Hennessy

When young researchers get together, one topic of conversation is “who supervised your PhD?” Back in the day, Rod Burstall was often named. Also mentioned were Robin Milner, Dana Scott and Gordon Plotkin. Then it would be my turn: “John Hennessy”. Who? Even today, while everyone has heard of Mark Zuckerberg and Bill Gates, few people can name the guy who is in charge of Google’s sprawling empire. But even those who got past the “who?” would then be asking “why?” Early years at Stanford I arrived in the autumn of 1977. It was not a good time for me. After a year of drifting, I found myself in the group of David Luckham and his Stanford Pascal Verifier. It consisted of a verification condition generator for Pascal coupled with a rewriting engine for proving the assertions generated. The user had to supply the rewrite rules, which had to be trusted: a major weakness. I worked on verifying list processing programs for a while (simple things like append and reverse), but came a cropper…