I once saw Leslie Lamport speaking at my university about TLA+. He recently had switched to Microsoft research. He started his talk with a short rant on how fo

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