Re: [tlaplus] Lean vs TLA+

[Stephan Merz <stephan.merz@xxxxxxxxx>]

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

On 17 Mar 2020, at 20:52, petarm@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

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/edf6cd0d-a753-4b5b-824c-c6d2a7623d69%40googlegroups.com.

--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/5736505E-EE27-4422-A8F4-23D73354E2E7%40gmail.com.