3 ms·

> There's no reason why one couldn't use a "code-level" (end-to-end) interactive proof tool to verify TLA+-like specs. Sure, and that is what TLA+, together wi

by pron 6y ago

> There's no reason why one couldn't use a "code-level" (end-to-end) interactive proof tool to verify TLA+-like specs. Sure, and that is what TLA+, together with its tools, aim to do. The problem is the relation between the spec, that you can precisely verify, and the program it aims to abstract. The advantage TLA+ has over code-level tools in this respect is that those tools use code as their specification language -- i.e. a formal language that is deterministic enough to efficiently compile/interpret and execute. But TLA+ allows you to specify at an arbitrary level, even levels with a lot of nondeterminism that precludes compilation, hence the difference between it and code. For example, in TLA+ you can say, suppose I have a subroutine that sorts, and then build and check your specification on top of that without actually writing a sorting routine that can be executed. Similarly, you can say something like, "some hashing function is used" without actually writing any specific hashing function. This way, you can write a specification that's small enough to be verified, yet captures the interesting aspects of a system that's made of too much code to verify at the code level.

zozbot234 6y ago
> But TLA+ allows you to specify at an arbitrary level, even levels with a lot of nondeterminism that precludes compilation, hence the difference between it and code. ... Similarly, you can say something like, "some hashing function is used" without actually writing any specific hashing function. This can also be done in many end-to-end tools. Typically, these tools allow for end-to-end proof based on the actual code; they don't require it.
- 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.

by pron 6y ago

zozbot234 6y ago

> But TLA+ allows you to specify at an arbitrary level, even levels with a lot of nondeterminism that precludes compilation, hence the difference between it and code. ... Similarly, you can say something like, "some hashing function is used" without actually writing any specific hashing function. This can also be done in many end-to-end tools. Typically, these tools allow for end-to-end proof based on the actual code; they don't require it.

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.