Re:Quint: A specification language based on the temporal log...
by abathologist on Wednesday December 20, 2023 @11:59AM
(#38710789)
Those are great questions! Let me add a one addendum to bugarela's excellent explanation, to help disambiguate these three formalism:
1. TLA[0] is a logical calculus invented by Leslie Lamport.
2. TLA+[1] is a formal specification language, also invented by Leslie Lamport, with semantics based on and reducible to TLA.
3. quint is also a formal specification language with semantics based on and reducible to TLA.
TLA+ can be understood as TLA extended with syntax sugar to help describe systems. On top of the logical calculus it adds niceties like `LET` bindings, syntax to represent common data structures, `CASE` expressions, a module system, etc. But TLA+ also exposes the underlying logic directly, making the language extremely expressive. The flip side is that nonsensical formulas which may not be checkable are pretty easy to write.
quint is a (programmer friendly) syntax that, while also desugaring to TLA, gives up expressivity to add the guardrails that we've found most helpful when specifying the systems we work on.
---
Please let us know if you have any followup questions :)
1. TLA[0] is a logical calculus invented by Leslie Lamport.
2. TLA+[1] is a formal specification language, also invented by Leslie Lamport, with semantics based on and reducible to TLA.
3. quint is also a formal specification language with semantics based on and reducible to TLA.
TLA+ can be understood as TLA extended with syntax sugar to help describe systems. On top of the logical calculus it adds niceties like `LET` bindings, syntax to represent common data structures, `CASE` expressions, a module system, etc. But TLA+ also exposes the underlying logic directly, making the language extremely expressive. The flip side is that nonsensical formulas which may not be checkable are pretty easy to write.
quint is a (programmer friendly) syntax that, while also desugaring to TLA, gives up expressivity to add the guardrails that we've found most helpful when specifying the systems we work on.
---
Please let us know if you have any followup questions :)
---
[0]: https://en.wikipedia.org/wiki/Temporal_logic_of_actions [1]: https://en.wikipedia.org/wiki/TLA%2B