Leslie Lamport: Video course on TLA+ • Hacker News Board

Re: Leslie Lamport: Video course on TLA+

#71

Post by ahelwer » Tue, Mar 21, 2017, 7:01 PM UTC

pron wrote: post #42

ahelwer wrote: post #19

Earlier quoted context omitted.

Amenable? Probably fairly amenable. It hasn't been done yet, though. It likely wouldn't be translation so much as proving that the existing code refines a TLA+ spec.

Showing that program code refines a TLA+ spec has been done for C and Java (although scalability is a different matter). C: http://link.springer.com/chapter/10.1007/978-3-319-17581-2_1... Java: http://ieeexplore.ieee.org/document/6042069 The C work seems more thorough.

Amazing! I hadn't heard of this, thank you. I'll add it to the Wikipedia article.

Re: Leslie Lamport: Video course on TLA+

#72

Post by chillitom » Tue, Mar 21, 2017, 7:39 PM UTC

hwayne wrote: post #33

djb_hackernews wrote: post #11

Earlier quoted context omitted.

I haven't watched the videos yet but I have been keeping my eye on TLA+ ever since seeing the whitepaper from Amazon and how they use TLA+ to spec out their distributed systems. As someone that works on distributed systems that could use some formality I think TLA+ could help, however, I have a hard time really understanding it. Do you know of any straight forward non-trivial examples? Something a little more complex…

I wrote an essay[0] about a non-trivial example I did at my company. We had to work with several finicky APIs and the TLA+ spec caught several critical bugs with it. Plus, it's purely a business logic system, so it's pretty concrete. If you're interested in learning more, I also wrote a beginner's guide[1] to the language, which contains concrete examples and exercises. [0] https://medium.com/espark-engineering-blog/…

Following your introduction now, it is a great quick-start tutorial, thanks for creating it.

Re: Leslie Lamport: Video course on TLA+

#73

Post by albertocsm » Wed, Mar 22, 2017, 4:06 PM UTC

qznc wrote: post #68

ahelwer wrote: post #4

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…

Why not YouTube? Clickable links are possible there as well.

plz check -> https://groups.google.com/d/msg/tlaplus/lAeWdCE9MLw/v03t3UEv...

Re: Leslie Lamport: Video course on TLA+

#74

Post by foxaal » Wed, Mar 22, 2017, 4:32 PM UTC

jdubray wrote: post #69

djb_hackernews wrote: post #11

Earlier quoted context omitted.

I haven't watched the videos yet but I have been keeping my eye on TLA+ ever since seeing the whitepaper from Amazon and how they use TLA+ to spec out their distributed systems. As someone that works on distributed systems that could use some formality I think TLA+ could help, however, I have a hard time really understanding it. Do you know of any straight forward non-trivial examples? Something a little more complex…

I have created the SAM Pattern [1] (State/Action/Model) based on my interpretation of TLA+. The goal is to make the semantics available to developers. Why not writing code as close as possible to the way it would be specified? SAM can also be used for stateful API/Microservice orchestrations [2] If you want a slightly more formal introduction to SAM and its relationship to TLA+ (again, based on my own interpretation)…

You wonder if there are code generation possibilities...

Re: Leslie Lamport: Video course on TLA+

#75

Post by jdubray » Fri, Mar 24, 2017, 7:58 PM UTC

foxaal wrote: post #74

jdubray wrote: post #69

Earlier quoted context omitted.

I have created the SAM Pattern [1] (State/Action/Model) based on my interpretation of TLA+. The goal is to make the semantics available to developers. Why not writing code as close as possible to the way it would be specified? SAM can also be used for stateful API/Microservice orchestrations [2] If you want a slightly more formal introduction to SAM and its relationship to TLA+ (again, based on my own interpretation)…

You wonder if there are code generation possibilities...

Actually, TLA+ (again the way I understand it), after nearly 20 years of MDSE, convinced me that I would very rarely need to generate code. It's a much better value proposition to write correctly factored code. TLA+ is one of the most amazing element of Computer Science. Everyone who writes code should have at least a basic understanding of it.

Re: Leslie Lamport: Video course on TLA+

#76

Post by Aclassifier » Mon, Mar 27, 2017, 7:10 AM UTC

I watched this very interesting and amusing series of videos and learned a lot from them. I was shown practical in-use and the motivation for mathematical syntax. I know Promela and CSPm some so I was curious to see more than a trivial example of some C lines becoming a TLA+ spec. I missed real-life examples of down-to-earth usage. The "Formal Development of a Network-Centric RTOS" book shows not only TLA+ but also why in their situation TLA+ was more suitable then other methodologies. Still, on TLA+ I miss the forest for the trees. I probably need more time with Lamport. I hope he's able to do a follow-up. (Or am I unfair here?)

Re: Leslie Lamport: Video course on TLA+

#77

Post by Aclassifier » Mon, Mar 27, 2017, 7:41 AM UTC

unboxed_type wrote: post #56

pron wrote: post #53

Earlier quoted context omitted.

TLAPS supports temporal reasoning. I've personally used it only for safety (inductive invariant), but to make sure it supports liveness, I just checked the following: THEOREM ASSUME NEW F, NEW G, F ⤳ G, F PROVE ◇G PROOF BY PTL and it works fine (PTL stands for propositional temporal logic). I suppose there are some things that aren't supported (TLAPS has quite a few missing features), but TLAPS is very new by proof-s…

Temporal reasoning is a lot more than that you mentioned, so by providing this example you can not conclude that TLAPS support temporal reasoning. I have read several papers of S.Merz, Lamport's student and now a researcher, who mentioned that there is no temporal reasoning apparatus available in TLAPS. Maybe something have changed since then but I found no evidence for this. > They just use the model checker, that c…

> Well I respect Mr.Lamport`s point, but to prove liveness you are almost doomed to use temporal logic.

I thought CSPm/FDR4 proved liveness on infinite event trails without temporal logic? Can't one extract "never" and "sooner or later" by just exploring the whole state space? Deadlock/livelock will never happen etc.

Re: Leslie Lamport: Video course on TLA+

#78

Post by unboxed_type » Tue, Mar 28, 2017, 10:58 AM UTC

Aclassifier wrote: post #77

unboxed_type wrote: post #56

Earlier quoted context omitted.

Temporal reasoning is a lot more than that you mentioned, so by providing this example you can not conclude that TLAPS support temporal reasoning. I have read several papers of S.Merz, Lamport's student and now a researcher, who mentioned that there is no temporal reasoning apparatus available in TLAPS. Maybe something have changed since then but I found no evidence for this. > They just use the model checker, that c…

> Well I respect Mr.Lamport`s point, but to prove liveness you are almost doomed to use temporal logic. I thought CSPm/FDR4 proved liveness on infinite event trails without temporal logic? Can't one extract "never" and "sooner or later" by just exploring the whole state space? Deadlock/livelock will never happen etc.

Yes, but what if you are unable to explore the whole state space due to its unboundedness? Then the only way I know is by deducing properties thru temporal reasoning.