Lean vs TLA+

[pet...@gmail.com]

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

[Stephan Merz]

Hello Petar,

I am not aware of a formal comparison, but I would assume that one can construct a model of the dependent type theory of Lean in set theory, and thus in TLA+. It could make for a nice research project to make this precise. In practice, both languages are of course highly expressive.

Regards,

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/edf6cd0d-a753-4b5b-824c-c6d2a7623d69%40googlegroups.com.

[Ron Pressler]

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

[Petar Maymounkov]

Thank you! Very informative.

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/R8FAk9tjRoc/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/cfc56f4a-98f6-4229-b5bd-9affc56f59a2%40googlegroups.com.