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.
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).
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+.
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.)
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.