Formal Specification and Taming Other People's Tech

Explore the practical applications of formal specifications in everyday system design through this conference talk. Discover how these tools can be used beyond academic settings and complex algorithms, applying them to common engineering tasks like configuring load balancers and message queues. Follow the real-world case study of a production system built with open-source technologies, learning how formal specifications helped untangle built-in assumptions and redesign the system to address growth challenges. Gain insights from Marianne Bellotti's experience in rescuing complex systems and building highly scalable services. Delve into topics such as the token bucket algorithm, state machines, impossible states, and the distinction between undesirable and impossible scenarios. Leave with a fresh perspective on how formal specifications can enhance your approach to system design and problem-solving in various engineering contexts.

Introduction
What is formal specification
Mariannes background
How to think about formal specification
The problem with formal specification
The token bucket algorithm
State machines
What states should be impossible
How do we prevent these states
What should this look like
Loops
Focus on Email Types
Undesirable vs Impossible
Recap
Inspiration