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.)
Thank you for the series!