TLA+ and Formal Methods (The Technium Podcast S02 E09)

The Technium

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?

1:08:19 Intrigued with Formal Methods

===== 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 =====

WEBSITE: https://technium.transistor.fm/
SPOTIFY: https://open.spotify.com/show/1ljTFMgTeRQJ69KRWAkBy7
APPLE PODCASTS: https://podcasts.apple.com/us/podcast/the-technium/id1608747545