It’s surprising to know that Dr. Leslie Lamport who wrote LaTeX is the creator of Paxos consensus algorithm and TLA.

Saying “Dr. Leslie Lamport who wrote LaTeX” might sound like “Larry Wall who wrote patch(1)”. It’s true but it shouldn’t be the first thing I have to mention.