Remember that this blog is coming from the Rigorous Systems Research Group (RSRG, aka “resurge”) at Caltech. The group has a fairly unique perspective on systems research, so you might wonder:

**If you were to pick the RSRG “ideal person,” whom would you pick?**

My ideal is Leslie Lamport, the Turing Award winner this year. Here’s why.

Leslie is among the most logically-rigorous computer scientists in the history of computer science, and he has done as much for developing the discipline of scientific, theory-based, rigorous computer systems implementation as any person. The combination of logical rigor and practical systems makes Leslie stand head-and-shoulders above everybody as the RSRG ideal.

Everything we do at RSRG deals with concurrency: communication networks, power systems, economics and information technology, cloud computing, distributed systems, control systems, and real-time analytic systems. The theoretical foundations of concurrent systems have two parts: (1) a logic that enables systems to be designed and analyzed rigorously, and (2) a collection of fundamental algorithms that lie at the heart of almost all concurrent systems. Several great computer scientists have built the foundations for the first part, and several have developed the foundations for the second. But only two or three in the history of computer science have done both, and Leslie is one of them.

TLA, the Temporal Logic of Actions, is a foundational logical structure for reasoning about concurrent systems. TLA was built partly upon work by logicians and theoretical computer scientists. TLA has had a huge impact on the actual practice of designing concurrent systems; all the Caltech students working on the theory of concurrent systems work on some variant of TLA.

A collection of core algorithms lies at the heart of the concurrent computing systems. These algorithms deal with fundamental issues such as: How can an agent in a multi-agent system correctly infer conditions about the states of other agents when agents can’t “see” other agents? How can agents adjust their clocks so that the times of the collections of agents are meaningful in practical ways? How can a collection of agents come to a consensus as to what happened? The RSRG course on distributed systems, CS 142, deals with these basic questions, and more than half of the algorithms taught in the course were authored or co-authored by Leslie.

Here’s a story that illuminates Leslie’s impact. I invited Leslie to give a talk at Caltech, and asked him to choose a topic. He asked me to find out what people at Caltech wanted him to talk about. So, I sent a standard message to everybody: What do you want Lamport to talk about?

I expected replies such as logics of concurrency, consensus algorithms and Byzantine failures. The huge majority of replies asked him to talk about LaTeX! So, I asked Leslie, apologetically, if he would give an unusual talk for a computer scientist at a research university: A seminar on how to write.

Leslie agreed. The room was packed. And packed with everybody: computer scientists, faculty and students from departments across campus, administrative assistants, and librarians. I had listened to several of Leslie’s talks, and each of them had been a truly perfect computer science talk: clear problem definition; clear, rigorous analysis, and substantial application to actual computing systems. I had never heard him give a talk on writing: on fonts, and subheadings, and footnotes.

He gave a brilliant talk. Several of the non-CS people told me afterwards how much they had benefited from that CS talk! Only some of them knew the huge amount of careful thinking and programming that went into LaTeX.

The RSRG ideal is a person who is mathematically rigorous, designs reliable systems, and creates beautiful programs. That ideal is Leslie Lamport!

Pingback: Rigor + Relevance | Rigor + Relevance beyond Caltech

Pingback: Rigor + Relevance | The 2014 Dijkstra Prize goes to…