Rigor + Relevance beyond Caltech

I’ve been busy traveling for most of the last month, so missed my chance for timely postings about a couple of exciting happenings that highlight how theory can impact practice. But, here are two that I can’t resist a quick post about, even if it is a bit late.

First, this year’s ACM SIGCOMM award recipient is George Varghese, for “sustained and diverse contributions to network algorithmics, with far reaching impact in both research and industry.”  I think that’s a pretty nice summary. George’s work has been an inspiration for me since grad school when I worked through his book on Network Algorithmics. He is one of the masters at finding places where theoretical/algorithmic foundations can have practical impact.  He’s also a master at communicating theoretical work to systems folks.  As a result, he’s one of the few folks that can consistently get theory-driven work into Sigcomm, which makes him the envy of many in the community.  It’s really great to see someone with such strong theory chops being recognized by the networking systems community.

The second piece of news is another highlight about the impact of Leslie Lamport‘s work.  Mani wrote a great post about him when he received the Turing award earlier this year, in case you missed it.  I finally got to see him give a technical talk at the Microsoft Faculty summit this year, and was excited to hear about how some of his work on model checking was finally getting adopted by industry.  He mentioned in his talk that Amazon was beginning to adopt it for some large internal projects, and was even budgeting time for development for TLA+, a formal specification language that Leslie invented.   After hearing this, I started to dig around, and it turns out that James Hamilton has recently blogged about incorporating TLA+ into the development of DynamoDB.

Continue reading


Leslie Lamport: The Ideal RSRG Scientist

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.

Continue reading