8 ms·

TLA+ is only "executable" in the same sense that an algebraic expression is executable. It's perfectly possible to write things on TLA+ that can not be simply e

TLA+ is only "executable" in the same sense that an algebraic expression is executable. It's perfectly possible to write things on TLA+ that can not be simply executed linearly. (These overlap to a great extent with the things which TLC rejects.) As a basic example, it's easy to write a statement with \A (unbounded universal quantification) whose truth can only be judged by a proof engine. Specification languages are explicitly not programming languages, for the core reason that programming languages dictate only what must occur; whereas specification languages can dictate what must not occur. It's not possible with a "specification" written using a programming language to determine what of a program is actually the specification, vs. what is an accident of the implementation.

AlotOfReading 2y ago
Being able to create systems by writing specifications and having the computer figure out how to execute them was basically the point of fifth generation programming languages. More relevant today, you can execute other "specification" languages like Coq and Idris because they support things outside the narrow feature set of specification usecases. TLA+ isn't executable and doesn't look like an imperative language because the authors don't want it to be, not because there's some universal line dividing specification languages from programming languages. It's also one of the biggest hurdles to TLA+ usage.
- RandomThoughts3 2y ago
  Coq is not a specification language. It’s an interactive theorem prover. The goal set is completely different.
  - AlotOfReading 2y ago
    Coq, specifically Gallina, is absolutely a specification tool. It's not only that, but it's one of the big use cases it's explicitly designed to support.
    - RandomThoughts3 2y ago
      No, it’s not. Gallina is not a specification tool in the way TLA+ is (even if coq calls it its specification language). Gallina is a language used to write mathematical statements which you intend to prove. It’s not designed to write specifications. Coq is definitely not a specification tool. You can probably prove a specification with it in the same way you actually can do symbolic manipulation with C if you really want to. It still remains an interactive prover.
      - auggierose 2y ago
        Of course Coq is also a specification tool. C compilers have been formally verified with Coq. So you have a spec for C in Coq.
        RandomThoughts3 2y ago
        "The C standard formalised in Coq" is literally the title of Robbert Krebbers's PhD, that gives you an idea of how usual and easy it was. The fact that you can formalise a specification in order to prove it doesn't make Coq a specification tool.
        auggierose 2y ago
        Oh, if you define specification as something that should be done by people without a PhD, you might have a point. I don't think software that needs specs should be done by people without a PhD. Jokes aside, I am not saying that Coq is an easy or simple specification tool. But of course it is a specification tool. Actually, it is one of the very few serious specification tools out there.
- pron 2y ago
  > Being able to create systems by writing specifications and having the computer figure out how to execute them was basically the point of fifth generation programming languages. Yeah, but in maths you can specify anything, including things that the computer is unlikely to figure out how to execute if it's possible at all. Programming languages of every generation are very useful, as is mathematics, even though they're not the same thing. > More relevant today, you can execute other "specification" languages like Coq and Idris because they support things outside the narrow feature set of specification usecases. Coq and Idris are very different in the way they're typically used, and I'd say TLA+ is much closer to Coq than to Idris (and is probably more popular than the two combined), but to "execute" anything the specification needs to be at a certain level that's detailed enough to produce a program, and oftentimes that is very much not what you want. It would be extremely useful to have a language that you could describe the various properties of a car and it would compile your specification into the design of a car (you would need to give it sufficient detail as there are choices to be made). But it would also be extremely useful to have a language that could be used to learn certain things about a car -- say, it's braking distance -- without specifying it in sufficient detail to actually build one. That is what maths is good for -- describing things at arbitrary levels of detail to answer relevant questions. For example, you may have a 5 MLOC distributed system, and you want to know if a certain kind of failure may lead to data loss. You could use TLA+ to describe just the relevant details to answer the question in, say, 200 lines of formulas. That you cannot compile those formulas into a working 5 MLOC piece of software is not a downside of mathematics, but rather the point. > TLA+ isn't executable and doesn't look like an imperative language because the authors don't want it to be And because it's not a language for programming but a language for mathematics, so it looks and feels pretty close to plain mathematics (only it's formal), as that's the obvious choice for writing mathematics.
  - Mathnerd314 2y ago
    > in maths you can specify anything, including things that the computer is unlikely to figure out how to execute if it's possible at all. Well, in TLA+ you can write programs that run forever (or at longer than you'll live) and don't do anything like "model check" or whatever you want to call executing TLA+, even though they are perfectly sound mathematically. This should make it clear that TLA+ is not maths.

AlotOfReading 2y ago

Being able to create systems by writing specifications and having the computer figure out how to execute them was basically the point of fifth generation programming languages. More relevant today, you can execute other "specification" languages like Coq and Idris because they support things outside the narrow feature set of specification usecases. TLA+ isn't executable and doesn't look like an imperative language because the authors don't want it to be, not because there's some universal line dividing specification languages from programming languages. It's also one of the biggest hurdles to TLA+ usage.

RandomThoughts3 2y ago
Coq is not a specification language. It’s an interactive theorem prover. The goal set is completely different.
- AlotOfReading 2y ago
  Coq, specifically Gallina, is absolutely a specification tool. It's not only that, but it's one of the big use cases it's explicitly designed to support.
  - RandomThoughts3 2y ago
    No, it’s not. Gallina is not a specification tool in the way TLA+ is (even if coq calls it its specification language). Gallina is a language used to write mathematical statements which you intend to prove. It’s not designed to write specifications. Coq is definitely not a specification tool. You can probably prove a specification with it in the same way you actually can do symbolic manipulation with C if you really want to. It still remains an interactive prover.
    - auggierose 2y ago
      Of course Coq is also a specification tool. C compilers have been formally verified with Coq. So you have a spec for C in Coq.
      - RandomThoughts3 2y ago
        "The C standard formalised in Coq" is literally the title of Robbert Krebbers's PhD, that gives you an idea of how usual and easy it was. The fact that you can formalise a specification in order to prove it doesn't make Coq a specification tool.
        auggierose 2y ago
        Oh, if you define specification as something that should be done by people without a PhD, you might have a point. I don't think software that needs specs should be done by people without a PhD. Jokes aside, I am not saying that Coq is an easy or simple specification tool. But of course it is a specification tool. Actually, it is one of the very few serious specification tools out there.
pron 2y ago
> Being able to create systems by writing specifications and having the computer figure out how to execute them was basically the point of fifth generation programming languages. Yeah, but in maths you can specify anything, including things that the computer is unlikely to figure out how to execute if it's possible at all. Programming languages of every generation are very useful, as is mathematics, even though they're not the same thing. > More relevant today, you can execute other "specification" languages like Coq and Idris because they support things outside the narrow feature set of specification usecases. Coq and Idris are very different in the way they're typically used, and I'd say TLA+ is much closer to Coq than to Idris (and is probably more popular than the two combined), but to "execute" anything the specification needs to be at a certain level that's detailed enough to produce a program, and oftentimes that is very much not what you want. It would be extremely useful to have a language that you could describe the various properties of a car and it would compile your specification into the design of a car (you would need to give it sufficient detail as there are choices to be made). But it would also be extremely useful to have a language that could be used to learn certain things about a car -- say, it's braking distance -- without specifying it in sufficient detail to actually build one. That is what maths is good for -- describing things at arbitrary levels of detail to answer relevant questions. For example, you may have a 5 MLOC distributed system, and you want to know if a certain kind of failure may lead to data loss. You could use TLA+ to describe just the relevant details to answer the question in, say, 200 lines of formulas. That you cannot compile those formulas into a working 5 MLOC piece of software is not a downside of mathematics, but rather the point. > TLA+ isn't executable and doesn't look like an imperative language because the authors don't want it to be And because it's not a language for programming but a language for mathematics, so it looks and feels pretty close to plain mathematics (only it's formal), as that's the obvious choice for writing mathematics.
- Mathnerd314 2y ago
  > in maths you can specify anything, including things that the computer is unlikely to figure out how to execute if it's possible at all. Well, in TLA+ you can write programs that run forever (or at longer than you'll live) and don't do anything like "model check" or whatever you want to call executing TLA+, even though they are perfectly sound mathematically. This should make it clear that TLA+ is not maths.