Formal methods with Hillel Wayne
Summary
Formal methods aren't mainstream because engineers rarely need 99% correctness—but AWS found data-losing bugs in DynamoDB using TLA+ that traditional testing missed. Lightweight formal methods like property-based testing offer a practical middle ground for most engineers without the overhead of full formal verification.
Key Takeaways
- AWS discovered critical data-loss bugs in DynamoDB and S3 using TLA+ that could have been missed by conventional testing, proving formal methods' value for systems handling customer data.
- The adoption barrier for formal methods is context-dependency—writing specifications becomes a nightmare when domain problems require extensive background knowledge, making it impractical for most codebases.
- Property-based testing and lightweight formal methods (like deterministic simulation testing) represent the practical sweet spot for most engineers, offering verification benefits without full formal verification overhead.
- AI-generated code may drive formal verification adoption, but full formal methods are overkill—lightweight approaches are more realistic for verifying machine-generated code at scale.
- The 'Crossover Project' investigated whether software engineers qualify as real engineers by interviewing 15+ traditional engineers, challenging the legitimacy debate in software development.
Related topics
Transcript Excerpt
Let's talk about formal methods. There's some sort of implicit mechanism in your brain that can [music] see that and know what the function is supposed to do. So step one of what I do with formal methods is asking can we take that implicit knowledge and make it explicit? Can we figure out what a function is supposed to actually be doing and write that down in a way that can be shown to anybody? >> Why are we not doing formal testing for everything? >> When you start talking about like most interesting domain problems, you have to pull in so much context that basically even writing what the function is supposed to do becomes a nightmare. the imperative program you're right that we'll get 99% of the time is probably good enough to use in almost all cases. >> One story I've heard and I think …