Thinking for Programmers (2014) [video]
channel9.msdn.com
channel9.msdn.com
As a general rule, it's excellent for projects where you have combinatorial explosion in state: the rules for state transitions are quite short, but number of behaviours is enormous. This is common in concurrency and distributed systems. When they're first starting out, lot of people think simple state machines are a good target for TLA+ specification, but this is not so. Generally for state machines the number of states is linear with respect to the number of rules you have, so you're better off using something like P which also generates code for you.
How difficult, in your opinion, would it be for someone with a math and CS degree (as educational background) to spin up on TLA+ in their spare time? I reasonably have 1-2 hours a night I can spend on this before I'd be eating into hobbies and social activities. I can think of several small projects that would be useful or will be started in a few weeks/months that I might be able to use as demonstrations of the utility of a system like TLA+ (requiring only an analysis of small portions of the protocol, for instance).
Specifying liveness is more difficult, since it involves temporal logic and other things I didn't cover in my degree. However, Lamport says (and I've found) 95% of specs will only need boilerplate temporal logic, so don't worry about it.
I taught myself through the book Specifying Systems, although Lamport now recommends the TLA+ Hyperbook.
Teaching yourself TLA+ then applying it to a work project to demonstrate its value to management is a good strategy. That is the approach I took, and having a concrete project to motivate study of TLA+ is very effective.
Another question, it seems they have a strong push to use the software tools (makes sense). A lot of the time that I'll have for this will be away from home, but not particularly busy (I tend to show up to places early so I often spend up to an hour at a bar/restaurant reading a book before friends arrive). In your opinion, would it be best for me to drag my laptop with me, or could I do a fair amount with paper and pencil and put it into the computer later?
It's an important topic and the substance is solid, and would be great to read a transcript, but I can't watch this whole thing through -- it's too slow-paced and pedantic. Is it just me or is there an epidemic in these technical talks where the speaker addresses the audience like they're 7th graders circa 1994? I.e., explaining what a computer is, what a program is, etc, in excruciating detail?
I totally get the importance of fleshing out concepts from the ground up, going from big to small, etc. But in this case, it seems like his hour-long talk could have been delivered in about 20 minutes with a lot fewer elementary examples.