About Me
My name is Marc Brooker. I like to build things that work, and do cool stuff. I like building big things. I also dabble in machining, welding, cooking, and skiing.I am an engineer at Amazon Web Services (AWS) in Seattle, where I work on agentic AI, especially safety and policy for agentic AI. Before that, I worked on EC2, EBS, databases, serverless, and serverless databases.
All opinions are my own.
Links
My Publications and Videos@marcbrooker on Mastodon @MarcJBrooker on Twitter
Is this blog written by AI?
How Amazon Web Services Uses Formal Methods
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.
Marc Brooker
The opinions on this site are my own. They do not necessarily represent those of my employer.
marcbrooker@gmail.com
RSS