Leslie Lamport to receive 2013 ACM Turing Award
acm.org
acm.org
He started his talk with a short rant on how formal proof of APIs is futile and a worthless task. Now, I don't know if he knew, but most of the professors sitting in the first row were precisely doing that.
I've never again seen a talk where the feeling of "just you wait for the Q&A" was in the room. Sadly, most questions were just low stabs about him being an MS employee now.
His talk back in 2011 on "What is Computation?" http://www.youtube.com/watch?v=BDPHfRuAFnU
Looks like they knew the result for a while before it went public.