4 ms·

Have you used Z? How does it compare to TLA+? I'm thinking of trying out TLA+ this holidays to spec a couple of algorithms at work.

• pron 10y ago
  > Have you used Z? How does it compare to TLA+? I haven't used it but I've seen some examples of it. In many ways it is similar to TLA+, and Lamport says it's a nice, mathematical language. From an aesthetic point of view, it is less elegant: it has many more built-in concepts. From a pragmatic point of view, I think it does not support concurrency at all. Before creating TLA+, Lamport had intended to add TLA to Z for concurrency. This was the result: https://research.microsoft.com/en-us/um/people/lamport/pubs/pubs.html#tlz https://research.microsoft.com/en-us/um/people/lamport/pubs/... Anyway, here's a comparison by Lamport: https://research.microsoft.com/en-us/um/people/lamport/pubs/spec-book-chap.pdf https://research.microsoft.com/en-us/um/people/lamport/pubs/... > I'm thinking of trying out TLA+ this holidays to spec a couple of algorithms at work. Cool. Apart from being very useful, it's a lot of fun.