When it comes to the “data” side of things — i.e. the “+” in TLA+ and the type level in Lean — as Stephan says, the two are probably as expressive for all intents and purposes. When it comes to computations, TLA+ is more expressive because TLA is more expressive than a lambda calculus; e.g. you can define “parallel or” in TLA but not in lambda calculus. Of course, you could deeply embed TLA in Lean and create a separate “world” where computations are described with TLA.
But these formal differences are not that important. What is important is the general purpose and design of the two languages. Lean, like Coq, Agda and Isabelle, is made primarily for research. It has rich meta-programming capabilities that allow defining new logics, and thanks to operator overloading it can be conveniently used to research serious “high” formal mathematics. TLA+, on the other hand, is designed for engineers who want to model and reason about large, complex real-world systems at arbitrary levels of detail. It is not flexible enough to allow researchers to define arbitrary new kinds of logic, and not convenient enough to be used for high formal mathematics, but learning it and using it for practical systems modeling is probably an order of magnitude easier than Lean. I think TLA+ main achievement is in creating a rich, expressive and powerful formal logic that is simple enough to be learned and used in practice by non-expert practitioners; in that regard, I consider it an exceptional achievement in the history of formal logic.
- Ron
On Tuesday, March 17, 2020 at 7:53:02 PM UTC, pet...@xxxxxxxxx wrote:
Hi Everyone!
I am wondering if there is a high-level statement that compares the
expressiveness of TLA+ vs that of LEAN.
Thank you
Petar