4 ms·

> Typically, these tools allow for end-to-end proof based on the actual code; they don't require it. TLA+ also allows for end-to-end proof, but it's not primar

by pron 6y ago

> Typically, these tools allow for end-to-end proof based on the actual code; they don't require it. TLA+ also allows for end-to-end proof, but it's not primarily designed for it. Because those other tools are primarily designed for it but not for arbitrary-level specification, they are drastically more complicated. This is necessarily the case. To allow execution, you must separate your computation level from your specification level (e.g. there is a distinct, syntactic spec/program or type/object divide), but that's not the case in TLA+. If you're familiar with, say, type-theory-based proof assistants, TLA+ is analogous to being at the type level only (except with an infinite hierarchy in both directions). In the time in took me to grasp Lean's type-theoretic universal quantification I was writing specifications of large, real-world systems in TLA+; I still find it hard to explain the meaning of universe-polymorphic operators like `id`. Plus, few if any of those languages have model-checkers, which also have a generally and drastically better cost/benefit than writing formal proofs. TLA+ has a very good proof assistant, but we rarely use them because writing a formal deductive proof after a successful model-checking is usually a terrible return on investment, unless your goal is publishing an algorithm rather than delivering a production system. Due to the scale limitation of sound verification, a system primarily designed for arbitrary-level specification and verification is more widely applicable than a system primarily designed for end-to-end verification, although the latter is certainly valuable in niche circumstances. It is, therefore, unsurprising that TLA+ is more commonly used in the field on systems that are too big/complex for feasible end-to-end verification (which is most "ordinary" software) than any of those primarily end-to-end tools. It is much easier to learn, especially for non-specialists, and thanks to the available model-checkers, it's also much easier to get results with.

ImprobableTruth 6y ago
>In the time in took me to grasp Lean's type-theoretic universal quantification I'm not sure what you mean? They work in the exact same manner as in normal predicate (higher order) logic. >I still find it hard to explain the meaning of universe-polymorphic operators like `id`. Uh, are you talking about the normal identity function? If one knows that they types have a level (universe) instead of a "type of all types" to avoid the 'set of all sets' paradox, I'm not sure what the issue would be.
- pron 6y ago
  > They work in the exact same manner as in normal predicate (higher order) logic. It is based on dependent products which you need to understand sooner-or-later (sooner, really), and are rather more intricate than FOL. > Uh, are you talking about the normal identity function? Ah, but that's the thing. It's not a function and it can't be (for the same reason you don't have an identity function in set theory). In TLA+ the meaning of terms is simpler, as there is a clear distinction between pure syntactic operators and domain objects (sets, but also functions). So in TLA+, you can have either: Id(x) ≜ x which is just parameterised syntax that does not denote any domain object, or perhaps you'd want: Id(S) ≜ [x ∈ S ↦ x] which is an operator defining the identity function on a given set. In Lean, however, universe u def id {α : Sort u} (a : α) : α := a which is similar in spirit to the second TLA+ definition, describes a rather complex object in the meta-domain.
  - ImprobableTruth 6y ago
    >It is based on dependent products which you need to understand sooner-or-later (sooner, really), Type-theoretic universal quantification _is_ the dependent product (/dependent function, a term I prefer). I assume you're talking about the Cartesian representation, but that's just one way to visualize it, the definition is not dependent on it. If you understand predicate logical quantification it's not necessary at all, since the introduction/elimination rules for type theoretic quantification are the same as for normal predicate logic quantifiers. >are rather more intricate than FOL Maybe in application and theoretical implications, but to grasp the concept you have just have to understand that it's relaxing the restriction on "what you can quantify over", which really isn't a huge jump I'd say. > Ah, but that's the thing. It's not a function and it can't be (for the same reason you don't have an identity function in set theory). Why would it not be a function? With set theory you have the issue that you can't take a set as an argument and have the codomain and it's elements be dependent on it, but that's exactly what dependent function types allow you to do. The universe U is a sort and A is a valid sort too, so forall A:U. forall a : A. A is a perfectly valid function signature and the term would just be (lambda A : U. lambda a : A. a). That doesn't strike me as any more complicated than your second TLA+ example. Sure, you have to deal with universe polymorphism, but I'd say that's compensated by the increased complexity from having to use syntactic operator. Lean's syntax to specify the universe U is admittedly pretty ugly, but the actual meta-theory isn't that complex I'd say.
zozbot234 6y ago
> Due to the scale limitation of sound verification, a system primarily designed for arbitrary-level specification and verification is more widely applicable than a system primarily designed for end-to-end verification I'm not sure what "designed for arbitrary-level specification and verification" boils down to here, or how it would differ in a useful way from an end-to-end-focused design. It seems like it would be relatively straightforward to embed something like, e.g. TLA in a proof assistant. The main features of TLA, viz. temporal logic and non-determinism, are well understood as special cases of modal logic, which can in turn be modeled via quantification on "possible worlds". So I'm not sure how a systen that only focuses on e.g. TLA is "more applicable" and "less niche" - But I would be happy to be proven wrong here.
- pron 6y ago
  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.

by pron 6y ago

ImprobableTruth 6y ago

>In the time in took me to grasp Lean's type-theoretic universal quantification I'm not sure what you mean? They work in the exact same manner as in normal predicate (higher order) logic. >I still find it hard to explain the meaning of universe-polymorphic operators like `id`. Uh, are you talking about the normal identity function? If one knows that they types have a level (universe) instead of a "type of all types" to avoid the 'set of all sets' paradox, I'm not sure what the issue would be.

pron 6y ago
> They work in the exact same manner as in normal predicate (higher order) logic. It is based on dependent products which you need to understand sooner-or-later (sooner, really), and are rather more intricate than FOL. > Uh, are you talking about the normal identity function? Ah, but that's the thing. It's not a function and it can't be (for the same reason you don't have an identity function in set theory). In TLA+ the meaning of terms is simpler, as there is a clear distinction between pure syntactic operators and domain objects (sets, but also functions). So in TLA+, you can have either: Id(x) ≜ x which is just parameterised syntax that does not denote any domain object, or perhaps you'd want: Id(S) ≜ [x ∈ S ↦ x] which is an operator defining the identity function on a given set. In Lean, however, universe u def id {α : Sort u} (a : α) : α := a which is similar in spirit to the second TLA+ definition, describes a rather complex object in the meta-domain.
- ImprobableTruth 6y ago
  >It is based on dependent products which you need to understand sooner-or-later (sooner, really), Type-theoretic universal quantification _is_ the dependent product (/dependent function, a term I prefer). I assume you're talking about the Cartesian representation, but that's just one way to visualize it, the definition is not dependent on it. If you understand predicate logical quantification it's not necessary at all, since the introduction/elimination rules for type theoretic quantification are the same as for normal predicate logic quantifiers. >are rather more intricate than FOL Maybe in application and theoretical implications, but to grasp the concept you have just have to understand that it's relaxing the restriction on "what you can quantify over", which really isn't a huge jump I'd say. > Ah, but that's the thing. It's not a function and it can't be (for the same reason you don't have an identity function in set theory). Why would it not be a function? With set theory you have the issue that you can't take a set as an argument and have the codomain and it's elements be dependent on it, but that's exactly what dependent function types allow you to do. The universe U is a sort and A is a valid sort too, so forall A:U. forall a : A. A is a perfectly valid function signature and the term would just be (lambda A : U. lambda a : A. a). That doesn't strike me as any more complicated than your second TLA+ example. Sure, you have to deal with universe polymorphism, but I'd say that's compensated by the increased complexity from having to use syntactic operator. Lean's syntax to specify the universe U is admittedly pretty ugly, but the actual meta-theory isn't that complex I'd say.

zozbot234 6y ago

> Due to the scale limitation of sound verification, a system primarily designed for arbitrary-level specification and verification is more widely applicable than a system primarily designed for end-to-end verification I'm not sure what "designed for arbitrary-level specification and verification" boils down to here, or how it would differ in a useful way from an end-to-end-focused design. It seems like it would be relatively straightforward to embed something like, e.g. TLA in a proof assistant. The main features of TLA, viz. temporal logic and non-determinism, are well understood as special cases of modal logic, which can in turn be modeled via quantification on "possible worlds". So I'm not sure how a systen that only focuses on e.g. TLA is "more applicable" and "less niche" - But I would be happy to be proven wrong here.

pron 6y ago
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.