An Introduction to TLA+
Note: This course is long since past, but was amazing. For more information on TLA+ training you should contact Hillel Wayne directly. If you'd like to tackle a problem where TLA+ might prove useful, you might enjoy my Rafting Trip course. --Dave
Overview
Most software flaws come from one of two places. When the code doesn't match our expectations, it could be that the code is wrong. Most software correctness techniques - types, tests, etc - are used to check the code. But it could instead be that the code is correct and our expectations are wrong: there's a fundamental error in our design. These errors, called specification errors, are some of the most subtle and dangerous bugs. They can span multiple independent programs, occur in convoluted race conditions, or depend on physical phenomena. Our regular tools simply can't find them.
Instead, we can find them with a specification language such as TLA+. TLA+ is the invention of Leslie Lamport, winner of the 2013 Turing Award and the inventor of Paxos and LaTeX. Instead of writing your design in code or plain English, you write it in TLA+'s special notation. Once you specify your core assumptions and requirements, it can explore how that system would evolve over time, and whether it actually has the properties you want. TLA+ is especially effective for finding bugs in concurrent code, distributed systems, and service architectures. And since it works on the design itself, we can fix issues before we've written a single line of code.
In this workshop, you will learn how the basics of TLA+ and how to apply to it real-world business problems. We focus in particular on how to design concurrent systens, such as microservices or client-server architectures. By the end of this class you should be able to write your own basic specs and use them to identify issues in your software designs.
Testimonial
"Every now and then, a course comes along that changes the way that you think about almost everything--this might be one of those courses. As a programmer, it is all-too-easy to get buried in the minute details of coding, libraries, and APIs. As an attendee at Hillel's first TLA+ course, I quickly came to realize that TLA+ is not a programming language focused on any of those things. Instead, it is a language for thinking about high level issues of software design, testing, and verification. Remember that tricky problem that made everyone cry on the Operating Systems midterm exam? TLA+ is exactly the sort of thing that will prove that your answer was wrong. In doing so, you'll quickly be staring in amazement. In short: if you want to become a better programmer, you should take this course."
-- David Beazley (author Python Cookbook, 3rd Edition).
Target Audience
You should have some experience programming, and some experience testing. While TLA+ is both powerful and accessible, it's aimed at experienced programmers. If you've ever had to deal with a race condition or a data I/O bug, then you are the target audience for course.
Instruction Format
Each course day runs from 9:30am - 5:30pm and mostly consists of hands-on projects interspersed with presentations. The main goal is to "learn by doing."
Prerequisites
This workshop is for experienced programmers. Prior familiarity with systems programming and concurrency topics is advised.
About the Instructor
The course is taught by Hillel Wayne. Hillel is the author of Learn TLA+ (http://www.learntla.com) and Practical TLA+ (Apress, est October 2018). He is in expert in the application of formal methods and works to make them an accessible, useful tool for people in startups and the industry. In his free time, he is a juggler and chocolatier. You can find him at http://hillelwayne.com or on Twitter at @hillelogram.