Leslie Lamport: Video course on TLA+

I viewed this original when he posted them on the newsgroup. I thought they were very well done, funny and enjoyable. I still haven't applied TLA+ into something at work however I enjoyed learning it nevertheless.

Great to see this here! I act as a TA for Dr. Lamport's TLA+ courses at Microsoft, and can answer any questions y'all have.

TLA+ in one sentence: it is a language used to write specifications, same as you might write a spec in English/your chosen informal language, except here you write your spec in basic mathematics; benefits of a formal specification language include freedom from ambiguity, model-checking, and even machine-checked proofs of correctness.

This language is a joy to use and I've found it really affects the way I think about system design.

Hmm, on the face of it that doesn't answer the question.

I'm about to start a new system that will have a state machine. The videos are really good to help to think about the problem. This guy didn't get a Turing Prize for nothing:-)

I won't even try to use TLA+ in my business context. Just will search for a good java library. Maybe these videos will help me to recognize a good one?

BTW, do any of my HN's fellows have a good Java state machine opens source library to recommend?

So how amenable is tla+ to automatic translation to an existing programming language?