When you find a flaw in a logic you thought was sound, and hopefully a fix for it, one obligation that follows is to show that what you are left with is a sound logic. But when the logic you are trying to fix is your logic, things are a bit different. It's something like learning that the gun that is pointed at you is loaded.
-Professor John Reynolds, Carnegie Mellon University
Professor John Reynolds from CMU came to give a talk about separation logic, an extension to Hoare logic and based in part on preliminary work by Burstall, that provides sequent rules for reasoning about imperative programs with shared, mutable data structures.
Oh, man, does that take me back. I was a research assistant from fall, 1993 through spring, 1994 in Uday Reddy1 and Sam Kamin's group, working on implementations of interpreters, type checkers, and type inference systems for various programming languages. I remember reading several iterations of Reynolds' Forsythe report between the 1988 original and the final 1996 version. As Matt Beckman once said of Matthias Felleisen during our year of study for the Ph.D. oral qualifying exams, "he is the name I have given to my pain".
'twas a good pain, though. I learned a bit about programming languages and semantics, much more than I knew. It was enough to realize that I was better suited to a balance between experimental and theoretical CS... and much better suited to machine learning and intelligent systems than to programming languages.
I remember hearing Reynolds' name on a daily basis back when Howard Huang, Matt Beckman, Jon Springer, and I were RAs for Sam and Uday. T.K. Lakshman, François Bronsard, and Rob Hasker were then very close to graduation and did not come to the weekly seminars on syntactic control of interference (SCI), functional programming type systems, and type systems for "clean, parallel C++" (a joint working group with Andrew Chien and Laxmikant Kale's CHARM group) that year.
This was also the year that Peter O'Hearn visited from Syracuse. At that time Reynolds had already gone to CMU (he arrived the year my uncle graduated). Interestingly, I never met Reynolds, only several of his collaborators.
Good times, good times. For a few minutes, I was a clueless 19-year old again, and all it took was a visit from the legendary computer scientist of my teenaged nightmares to bring it all rushing back.
Dave Schmidt averred that:
Reynolds is the most important computer scientist to visit this department since Tony Hoare visited in 1990 and Dana Scott visited in 1994.
which sounds just about right. (We've had some prominent intelligent systems people in recent years, but Clark Glymour, also of CMU, is a philosopher of science first and Prakash Shenoy is officially in the School of Business at KU.) Besides which, due to his work in the 1960s on compilers and computational science, and his arc from Harvard to Stanford to CMU, rivalled by only a few preeminent researchers such as Persi Diaconis2, Reynolds has arguably one of the highest impacts in CS in general.
Reynolds definitely sits high on the list of the most famous CS and AI people I've ever heard speak:
- Richard Karp (ACM Turing Award, 1985) - at Hopkins, in 1992
- Butler Lampson - (ACM Turing Award, 1992) at UIUC, as a Gillies lecturer
- Juris Hartmanis (ACM Turing Award, 1993) - at UIUC in 1997, when he was head of NSF-CISE
- Judea Pearl - at Hopkins, on 10 Nov 1992
- David E. Goldberg - one of my profs for 5 years (1993-1998) and a member of my "all-star committee", as Jesse Reichler called it
- Sir Roger Penrose - at UIUC in 1994, when he came to talk about Shadows of the Mind and The Emperor's New Mind
- Shun-Ichi Amari - at WCNN-1996
- David Heckerman - every UAI I've been to (1997-1998, 2001-2003); one of the most prolific Bayesian networks people
- Stuart Russell - at AAAI-1998, IJCAI-2001, AAAI-2002, and UAI-2003
- Ruzena Bajcsy - at AAAI-1998 (I know her children, both computer scientists, but didn't realize at the time that they were her children)
- John Koza - at GECCO-2000
I've actually met Karp, Pearl, Goldberg, Penrose, Amari, Heckerman, Russell, Bajcsy, and Koza. Oddly enough, I've never met some of the Turing award winners who are friends of my family or personal friends: my uncle's advisor, Raj Reddy (1994); Jim Gray (1998), whose talk I missed at the 2003 Atanassoff Centennial Symposium at Iowa State; Andy Yao (2000), a UIUC alum; or any of R, S, or A (2002). Also, you'd think I'd have met Amir Pneuli (1996), whose work on temporal logic with Zohar Manna is quite famous. Finally, I've missed at least two, possibly three, chances to hear Hofstader.
1 Uday, now head of the CS department at the University of Birmingham, later joined Peter O'Hearn at Queen Mary and I've since learned that he spent a sabbatical at Imperial and Glasgow. Does that qualify as a Brit reference? (/me pays pun fund)
2 Professor Diaconis, the banquet speaker at UAI-2002, bounced between Harvard and Stanford for three decades before finally settling at Stanford.