Marc's Blog

How Amazon Web Services Uses Formal Methods

Now in CACM.

How Amazon Web Services Uses Formal Methods is in this month's Communications of the ACM. This version isn't changed much from the versions that have been online for a few months, but it's great to see it get some more attention.

In the same issue of CACM is Leslie Lamport's Who Builds a House without Drawing Blueprints?. Fans of his writing won't find anything new in there, but it's a perspective and opinion that I love to see gain more traction.

We think in order to understand what we are doing. If we understand something, we can explain it clearly in writing. If we have not explained it in writing, then we do not know if we really understand it.

And the conclusion:

Thinking does not guarantee that you will not make mistakes. But not thinking guarantees that you will.

It's a very good take on the subject. As our experiences at Amazon have shown, specification can be an extremely powerful tool in the system designer's and programmer's toolbox. It's even more useful as a team member, where the ability to communicate particularly tough ideas formally and concisely really helps collaboration.

Other good formal methods reading this week:

• A post by Mark Callaghan about using Spin for MySQL development. I haven't spent as much time with Spin (or Promela) as I would like, but it's very interesting.
• Adrian Colyer wrote a good mini-series this week on SPL, one looking at deep bugs in distributed systems and the other at the background of SPL. He finished up with Lineage-Driven Fault Injection. All three posts, and the papers behind them, are good reading.
• Not really from this week, or this decade, or century, but still worth it - Lamport's article brought me back to What Good is Temporal Logic?, one of my favorite papers from him. It's extremely interesting to see how his thinking, and chosen framing, has evolved in the last 32 years.