Marc's Blog

About Me

My name is Marc Brooker. I've been writing code, reading code, and living vicariously through computers for as long as I can remember. I like to build things that work. I also dabble in machining, welding, cooking and skiing.

I'm currently an engineer at Amazon Web Services (AWS) in Seattle, where I work on databases, serverless, and serverless databases. Before that, I worked on EC2 and EBS.
All opinions are my own.


My Publications and Videos
@marcbrooker on Mastodon @MarcJBrooker on Twitter

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: