Leslie Lamport revolutionized how computers talk to each other. The Turing Award-winning computer scientist pioneered the field of distributed systems, where multiple components on different networks coordinate to achieve a common objective. (Internet searches, cloud computing and artificial intelligence all involve orchestrating legions of powerful computing machines to work together.) In the early 1980s, Lamport also created LaTeX, a document preparation system that provides sophisticated ways to typeset complex formulas and format scientific documents. In 1989, Lamport invented Paxos, a “consensus algorithm” that allows multiple computers to execute complex tasks; without it, modern computing could not exist. He’s also brought more attention to a handful of problems, giving them distinctive names like the bakery algorithm and the Byzantine Generals Problem. Lamport’s work since the 1990s has focused on “formal verification,” the use of mathematical proofs to verify the correctness of software and hardware systems. Notably, he created a “specification language” called TLA+ (for Temporal Logic of Actions), which employs the precise language of mathematics to prevent bugs and avoid design flaws.
