Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Leslie Lamport: Video course on TLA+

lamport.azurewebsites.net

Post reply on HN
Print view View original

61–70 of 78 posts

Re: Leslie Lamport: Video course on TLA+

#61

Post by pron »

agentultra wrote: post #60
pron wrote: post #40

Earlier quoted context omitted.

This is a complicated question. I am currently writing a blog post series on the theory of TLA+ that I will publish in May that, among other things, touches precisely on this point. But I will try to quickly point out some areas of difference, but the most important thing to remember is that both Coq and TLA+ -- as far as specifying and verifying software is concerned (not general math) -- are universal formalisms. U…

I too have a series of blog posts on TLA+ and verification in general aimed at working programmers. I'm giving a talk next month at a local developers' meet up on formal specifications and will probably cover TLA+ mostly (or maybe Dafny?). I'd love to read your posts. Is there a url or twitter account where I can get updates on your work?

I expect to publish the posts starting in mid-May. My twitter handle is pressron

Re: Leslie Lamport: Video course on TLA+

#62

Post by rebootthesystem »

qznc wrote: post #49
rebootthesystem wrote: post #13

In many ways this is what APL was originally about. Ken Iverson used it to describe the operation of early IBM computers while at IBM.

"A Formal Description of System/360" Readable (kind of) here: https://www.yumpu.com/en/document/view/40763566/a-formal-des...

Nice find!

Re: Leslie Lamport: Video course on TLA+

#63

Post by neves »

whitenoice wrote: post #23
neves wrote: post #8

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 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

It looks nice, but overkill for my application. For now I have no need for distributed systems, probably some concurrency in the near future.

Re: Leslie Lamport: Video course on TLA+

#64

Post by nchuhoai »

Possibly a side question:

What do people think of the format? I have off and on been thinking about a format where the video is the main highlight, but is supported, like this one, with links and other media to make it a more engaging experience. Are there other use cases that you think this would be conducive for?

Re: Leslie Lamport: Video course on TLA+

#65

Post by sdbbp »

In my experience, writing a formal specification _once_ in TLA+ has shaped my mindset around architecture, implementation, and verification of distributed systems for the last 19 years. It's easier to provide feedback on most informal architecture specifications. It is easier to implement to a specification so as to have a higher confidence of compliance. It is easier to consider the state space of an architecture (distributed system) when in a testing/verification role.

Re: Leslie Lamport: Video course on TLA+

#66

Post by macintux »

noblethrasher wrote: post #12
rhizome wrote: post #6

Earlier quoted context omitted.

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

The claim is that what he is about to say is worth your attention . Achievement of the highest professional accolade for the very stuff that he plans to discuss is literally prima facie evidence in support of that claim.

The transcription ("turning award" instead of "Turing award") makes it easier to miss the key point.

Re: Leslie Lamport: Video course on TLA+

#67

Post by a-saleh »

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…

I understand that I wouldn't be able to actually run the TLA+ specs, but is there some way how would I be able to run i.e. some of the traces against a live system?

I do QA work and for quite some time I have been intrigued by property based testing. But we are usually testing lot of interconnected micro-services and when I tried to define test-scenario in i.e. quick-check, the end-result was always too complicated to maintain.

I basically tried to do a similar thing to John Hughes "Mysteries of Dropbox" paper.

It seems that with temporal logic it would have been much easier to specify the expected behavior of the program and then use the generated trace to instrument the live service and check that all of the properties still hold.

Re: Leslie Lamport: Video course on TLA+

#68

Post by qznc »

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.

Re: Leslie Lamport: Video course on TLA+

#69

Post by jdubray »

djb_hackernews wrote: post #11
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…

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) I gave this lecture last month [3].

[1] http://sam.js.org

[2] http://www.ebpml.org/blog15/2015/06/designing-a-reliable-api...

[3] http://cloudsentinel.com/sam-state-machines-and-computation....

Re: Leslie Lamport: Video course on TLA+

#70

Post by ahelwer »

a-saleh wrote: post #67
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…

I understand that I wouldn't be able to actually run the TLA+ specs, but is there some way how would I be able to run i.e. some of the traces against a live system? I do QA work and for quite some time I have been intrigued by property based testing. But we are usually testing lot of interconnected micro-services and when I tried to define test-scenario in i.e. quick-check, the end-result was always too complicated t…

This is a really good idea! It's been pitched inside where I work in Azure, but not yet implemented anywhere (to my knowledge). The basic idea is you have a TLA+ spec of your system, then you run the model-checker in "simulation" mode to generate random execution traces. You take these generated execution traces, and, according to some predefined correspondence between the actions in your TLA+ spec and some API call in your code (a node becoming inaccessible or a message being sent, for example), run the execution traces on your real-world system.

I'd love to see you implement this and write about your experiences.

Post reply on HN