[deleted]
Leslie Lamport: Video course on TLA+
21–30 of 78 posts
Re: Leslie Lamport: Video course on TLA+
#22Earlier quoted context omitted.
Kind of an out of left field question: Lamport appears in a little square of video occasionally overlaid on the slides and sometimes full screen. As far as I can tell, he never recycles an outfit and seems to switch head gear regularly. The switch is often between segments that are quite short. It feels almost like an intentional joke. Do you think that is the case? Or just even short segments were recorded on differ…
Haha yep, it's intentional. He has a sense of humor like that. Famously, he first presented his paper on the Paxos algorithm dressed like Indiana Jones with the fictional backstory of the algorithm being an archeological discovery of the ancient parliamentary systems of the Greek island of Paxos.
The paper is more of the same: https://www.microsoft.com/en-us/research/wp-content/uploads/... addmitadly, it's also fairly difficult to follow the random interspersed bits of Greek.
Re: Leslie Lamport: Video course on TLA+
#23I'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 recom…
You could use akka[1] library to build a state machine, actor model is great for building state machines [2]. I have built one in the past using akka. Library is pretty robust and well maintained.
[1] http://akka.io [2] http://erlang.org/documentation/doc/4.8.2/doc/design_princip... [3] http://doc.akka.io/docs/akka/current/java/fsm.html
Re: Leslie Lamport: Video course on TLA+
#24Great 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…
[deleted]
Re: Leslie Lamport: Video course on TLA+
#25Great 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…
attended a course where @ahewler TA'd. can attest, he is awesome! disclaimer - msft engineer.
Re: Leslie Lamport: Video course on TLA+
#26Great 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…
attended a course where @ahewler TA'd. can attest, he is awesome! disclaimer - msft engineer.
Aw, thanks!
Re: Leslie Lamport: Video course on TLA+
#27Just finished the first video. Very nicely done. The website is nicely done too, not obtrusive and makes the learner to focus on the video. +1
Re: Leslie Lamport: Video course on TLA+
#28Great 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…
What role/job title usually writes the TLA+ specs at an organization?
Re: Leslie Lamport: Video course on TLA+
#29Great 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…
What role/job title usually writes the TLA+ specs at an organization?
I've yet to come across a TLA+-specific job title, although would love to be surprised. Usually it's the same people writing the spec, or engineers who produce a TLA+ spec from a provided informal-language spec.
Re: Leslie Lamport: Video course on TLA+
#30Great 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…
Dr. Lamport does courses at Microsoft? More details please.