Farewell to Amir Pnueli

I just learned from Comm ACM that we recently lost Amir Pnueli to a brain hemorrhage.  Dr. Pnueli coined the term "reactive system" and revolutionized program verification through his work in temporal logic.  That is not what I will remember.  I had the privilege of meeting Dr Pnueli while working on a task force on formal methods education.  He gave a talk and managed in 5 minutes to clearly cover what takes me 2 lectures in my formal methods class.  When I had the opportunity to speak at length with him, he was gracious and valued what I had to say.  In his obituary in Comm ACM, one of his students described precisely what I felt - "people loved working with him because he made them feel smart."  That is what I will remember.