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.
James is a vice president of the Amazon web services team, and you can find his whole post here. But, I guess the relevant quote is:
“I’ve always been somewhat skeptical of formal methods in that some bring too much complexity to actually be applied to commercial systems while others tend to abstract much of the complexity but, in abstracting away complexity, give up precision. TLA+ and PlusCal appear to skirt these limitations and we believe that having the core and most fundamental algorithms on which DynamoDB is based provably correct helps speed innovation, ease the inherent complexity of scaling and, overall, improves both the customer experience and the experience of engineers working on the DynamoDB system at AWS.”
This is the message that formal methods folks have been pushing for a long time: You don’t need these tools for everything (or even most things), but once code reaches a certain level of complexity/importance, then formal methods can actually speed up the development process. Hopefully, the experiment continues to be successful!