‘I Was Worth Trying to Help’
Leslie Lamport, GSAS MA’63, PhD’72, H’17
Computer scientist Leslie Lamport, GSAS MA’63, PhD’72, H’17, never thought mathematics was rigorous — until he came to Brandeis.
Geometry proofs that relied on pictures felt like sleight of hand. Even calculus struck him as analytically deficient.
Then he took a class with Richard Palais, now a professor emeritus of mathematics. Palais approached calculus with a thoroughness he’d never seen before. “Dick made me realize that if I understood any math, I could reason completely rigorously about it,” Lamport says.
Lamport went on to develop brilliant algorithms using the mathematical approach he learned at Brandeis. In a series of papers starting in the 1970s, he devised the mathematical formulas that undergird distributed computer networking, the process whereby multiple computers talk to one another without relying on a coordinating central computer.
These formulas are among the algorithms that run the World Wide Web. Distributed networking allows millions of computers to share data, perform computations, and make decisions, without the time-consuming process of calling into a central node for instructions. It also ensures the system can keep going if any computers fail.
As pioneering computer scientist Robert Taylor has said, “You like using the internet, you owe Leslie.”
In 2013, Lamport received the A.M. Turing Award, computer science’s Nobel Prize.
Now a distinguished scientist at Microsoft Research Lab, Lamport says he is especially grateful to Brandeis’ math department for an act of faith: It accepted him back after he dropped out.
Shortly after earning his master’s, Lamport left to study music and, for several years, taught math at a small Vermont college. He eventually realized math was for him after all. “Brandeis realized I was very smart, and I was worth trying to help,” he says.
For the past 25 years, Lamport has worked on developing a system of tools and techniques for computer programming called TLA+ (Temporal Logic of Actions). It asks programmers to create an outline, expressed in mathematical theorems, that explains what the software program will do and how it will do it.
In many ways, it requires them to employ the same analytical rigor Lamport discovered at Brandeis.