TLA+ in Practice and Theory, Part 3: The Temporal Logic of Actions | Hacker News Reader

TLA+ in Practice and Theory, Part 3: The Temporal Logic of Actions

pron.github.io

130 pointspron7 comments

Hah, the tidbit about Lamport having a different view from Hoare/Milner about revealing the control state is really spot-on. Coming from a mostly process-algebra-oriented background (CSP, CCS and the like), TLA+ can sound both familiar and alien.

Thank you for the series!

As I will discuss in part 4, the algebraic approach most similar to TLA is Ralph-Johan Back's and Joakim von Wright's refinement calculus/algebra. However, AFAIK, it doesn't (yet?) handle concurrent algorithms, whereas in TLA concurrent and sequential algorithms are formally indistinguishable (they are only distinguishable by how a reader informally interprets the formula; see the mention of "processes are in the eye of the beholder" in the post).

Very well written! I think more CS educations should devote more time to mathematical logic and its usefulness in CS. :)

I tried to quickly grep what 1st part is about and then 3rd, but failed. Can someone please summarize these documents?

Edit: oh, there is wikipedia article on TLA+.

https://en.wikipedia.org/wiki/TLA%2B

As the author, let me summarize. TLA+ is a language (not a programming language!) that allows you to describe software systems mathematically and reason about them, meaning, write which properties you claim they have (e.g., every user request will get a response) and verify that they indeed satisfy those properties. TLA+ is used by Amazon to help design their AWS services. This series is a deep dive into the mathematical theory and design principles of TLA+.

Great series! Thanks so much for writing it!

Noticed a few typos: "there exits"; "adding more states so to it"; "many possible future"; "talking about expression". In note 14, the asterisks are being lost, with the text between them italicized. Note 15 is immediately followed by a comma splice; maybe you wanted "so" after the comma? Note 16 is also screwed up.

(Calling it a night. Will continue at some point. Would love to chat further; email in profile.)

Thanks! Fixed. A good place to discuss this at length (or note additional mistakes) is the Reddit link at the very bottom of the post.

Reply on news.ycombinator.com