Sat down with a good friend who’s in math + economic history.
He’d taken me to school at the gym, introducing the Thai boxing exercise “kick the heavy bag” 45-seconds-per-leg. Brutal. Loud. I can perhaps recommend it. Afterwards at Nobes, enjoying a traditional meal of potatoes, gravy and vegan kålpudding, he asked me whether math is any use to career programmers.
I hemmed, I hawed. Most programmer activity is not about math. Statistics? Algorithms? Graph theory?
And then I tried to explain TLA+. I failed hard at that, so this short note is a link to better material than I was able to mumble up during eating.
TLA+ is:
a formal specification language developed by Leslie Lamport. It is used to design, model, document, and verify concurrent systems.
the TLA+ wikipedia article
The wikipedia article is good. Turns out, Lamport did us one better, he put together a full video course:
“This is the first lecture of the TLA+ video course”, a sun-kissed Lamport intones in the first few seconds. Excellent!
Then, he warns the viewer, that they should consume this course together with the multimedia he has created, at his website. TLA+ Course Lecture 1.
He’s right.
Having watched a few of these caring, teaching, and (mildly) funny videos, I’m becoming a fan. Well-made timed multimedia cues are great. Being told when to stop watching, and downloading a paper, or learning something else – it works well.
(The material is darn interesting.)
Resources made by Lamport on TLA+ abound, and I’m not doing you a service by trying recommend anything less than the real video thing. Any other code repository or tooling he’ll tell you about. He’ll tell you about it while dressed in clown clothes and corny outfits.
For the very interested, and text-oriented, there’s also the hyperbook. A series of interlinked PDF resources, which one can peruse to learn about TLA+. I read a bit of that first, and then switched over to the video presentation. Both are good.
Now, I hope this small note has alerted you to the existence of tons of TLA+ material online, and that you enjoy a whiff of that at some point.