First, UX is not (mostly) about the chosen theory, and the fact that all sufficiently rich formalisms can all be embedded in one another (indeed, TLA has been e

First, UX is not (mostly) about the chosen theory, and the fact that all sufficiently rich formalisms can all be embedded in one another (indeed, TLA has been embedded in Isabelle/HOL, and Coq) doesn't mean that they all have the same UX, just as the fact that Assembly, C++ and Python can all interpret one another doesn't mean that their UX is the same. (And that TLA+ focuses "only" on TLA means just as much as saying Agda focuses "just" on lambda calculus; you can embed the lambda calculus in TLA just as you can vice-versa). TLA+ is specifically designed for engineers -- not logicians -- to specify digital and hybrid systems rather than explore formal mathematics in general. Plus, the tooling makes a world of difference. Second, as I tried explaining before, all formalisms that focus on end-to-end verification must be more complex, because they must be programming languages; this means that they need a well-defined portion of their syntax to be executable. For example type-theoretic formalisms have distinct categories for the object level and the type-level, the type level not being executable (although in some very specific circumstances, it's possible to automatically synthesise an inhabitant from its type). TLA+ is not a programming language. It has no specific syntactic category that can be executed, and there is no distinction between a type level and an object level. There is just a type-level, you like. Moreover, there's an infinite lattice of formulas, and the simple logical implication, A ⇒ B, means that A implements or refines B, or that B is an abstraction of A (if you're familiar with types, this could either correspond to A being an inhabitant of B or A being a subtype of B, except there is no distinction between the two). In fact, there's a theorem that says that if B is an abstraction of A, then you can prove A^ ⇒ B, where A^ is A with some substitutions. If you're interested, I have a rather long text, written as a series of blog posts, about TLA+'s design of the theory and its ergonomics: https://pron.github.io/tlaplus https://pron.github.io/tlaplus. Parts 3 and 4 focus on the computational aspect, while part 2 talks of the data aspect.