Feeling of Computing The Case for Formal Methods: Hillel Wayne
Apr 11, 2019
Hillel Wayne, a technical writer and expert in formal methods like TLA+ and Alloy, shares fascinating insights into the world of software verification. He introduces the four quadrants of formal methods, exploring practical applications and current limitations. Hillel emphasizes the importance of specifications and clarifies the distinction between verification and validation. He also discusses the challenges of automated code generation and how TLA+ serves as an effective tool for high-level system specification, while cautioning that it isn't a cure-all for software problems.
AI Snips
Chapters
Books
Transcript
Episode notes
How Hillel Discovered TLA+
- Hillel found TLA+ after hitting a tricky distributed-systems bug at a web company and it solved his problem.
- He then wrote tutorials, gave talks, and authored a book which launched his formal-methods career.
Four Ways To Think About Formal Methods
- Formal methods split into specifying and verifying across code and design, forming four broad quadrants.
- Specification describes desired behavior; verification shows code or design matches that description.
Formal Verification Aims For '100%'
-
