TLA+ and Formal Methods (The Technium Podcast S02 E09)
TLA+ is a language for formally modeling and verifying the correctness of programs, especially concurrent and distributed ones. We discuss how it could be used to improve the practice of software engineering and what it would take for formal methods to gain more popularity.
TLA+ is a language for formally modeling and verifying the correctness of programs, especially concurrent and distributed ones. We discuss how it could be used to improve the practice of software engineering and what it would take for formal methods to gain more popularity.
Links/Resources:
- TLA+ Homepage https://lamport.azurewebsites.net/tla/tla.html
- https://learntla.com/introduction/
- https://lamport.azurewebsites.net/video/videos.html
- https://lamport.azurewebsites.net/tla/tutorial/contents.html
- https://lamport.azurewebsites.net/tla/industrial-use.html
- https://cacm.acm.org/magazines/2015/4/184701-how-amazon-web-services-uses-formal-methods/fulltext
Chapters:
0:00 Intros
2:14 What is TLA+?
5:10 Bugs in Concurrent and Distributed Programming
12:58 What's it like to use?
19:09 Global State Machine
20:34 Testimonials of Industrial Use Cases
24:56 Why is it not more popular?
27:32 How do we currently design our programs?
37:16 Everyone is a distributed systems programmer now
41:29 Thick client app management
49:47 Can haz use for Security?
53:08 TLA+ is for the design, not implementation
59:35 TLA+ all the things
1:02:55 Formal methods in Crypto?
===== About “The Technium” =====
The Technium is a weekly podcast discussing the edge of technology and what we can build with it. Each week, Sri and Wil introduce a big idea in the future of computing and extrapolate the effect it will have on the world.
Follow us for new videos every week on web3, cryptocurrency, programming languages, machine learning, artificial intelligence, and more!
===== Socials =====
