I once saw Leslie Lamport speaking at my university about TLA+. He recently had switched to Microsoft research.<p>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.<p>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.