[colanderman]

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]

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.

[pron]

> 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]

> 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.

[pron]

I don't understand the order of your implication. You can use maths (say, some ZFC formalism) to specify the execution of any Python or Java or C program and even write a software tool that executes it. It's the converse that isn't true: You cannot write a Python or Java or C program that accurately expresses many mathematical theorems (e.g. you can only express computable numbers in a program). I.e. the expressivity of mathematics includes that of programming, but not vice versa.

In TLA+ you can express every theorem in ZFC, but that doesn't mean you can automatically prove or disprove every proposition or even every theorem, because that is indeed a limitation of mathematics. There are also lots and lots of theorems you can state and prove in TLA+ yet not prove automatically with the TLC model-checker (or, indeed, with any known automatic proof method). That is a limitation of TLC (or of any known automatic proof methods), but not one of TLA+.

[Mathnerd314]

Actually the converse is true: Lean and other projects have formalized most mathematical theorems. But it is an "additive" process - it is easy to paraphrase a formal Lean theorem as colloquial mathematics, but it is hard to formalize colloquial mathematics in Lean. Some of this is due to Lean not being as developed as it could be, but also there is simply that some "theorems" in mathematics are simply "wrong" in that they make unstated assumptions and handwave away important parts of the proof. It is in this sense that programming is less expressive than mathematics, in that you can get away with writing things in mathematics that you can't get through a theorem checker. And this is conversely why I say that programs for theorem checkers are executable - the requirement to pass a theorem checker imposes constraints on proof structure and such that is not found in the "natural" language of mathematics. The lack of these limitations is what I would say the limitation of mathematics is, that even well-known proofs are not necessarily completely "true" due to unstated assumptions.

Now regarding TLA+ vs TLC, I am not clear what the utility of a TLA+ program that cannot be checked with TLC / TLAPS / etc. When you say "prove" a TLA+ program I first thought this was formally checking it with TLC / TLAPS / etc. But it seems you have a different notion of proof, some sort of handwaving "it looks right" notion. From my perspective this reduces a TLA+ program to a piece of writing, since nothing automated can be done with it. You might as well say "You can express every theorem in ZFC in Java by writing it in a comment" - it is not an informative observation. The interesting TLA+ programs are the ones that can be checked with TLC / TLAPS / etc., and to the extent one can work with these programs programmatically, TLA+ is a programming language.

[pron]

> And this is conversely why I say that programs for theorem checkers are executable - the requirement to pass a theorem checker imposes constraints on proof structure and such that is not found in the "natural" language of mathematics.

But TLA+ formulas not programs for a proof checker. There is a model checker than can check some subset of TLA+ and a proof checker that can check some TLA+ proofs (if they're detailed enough to be checked), but you can even write proofs in TLA+ that TLAPS cannot check.

> Now regarding TLA+ vs TLC, I am not clear what the utility of a TLA+ program that cannot be checked with TLC / TLAPS / etc.

First, there is no such thing as a TLA+ "program". You write mathematical definition and state propositions. Second, that's like saying that it's not clear what the utility of any formal mathematics without tools, but formalisms were invented long before there were computers.

You can prove things without having them checked by a proof checker -- indeed that is how nearly all mathematical theorems have been proven -- and it's a rigorous process that isn't at all the same as things just "seeming" right.

Obviously, most of the practical usage of TLA+ involves use of TLC, some smaller amount involves the use of TLAPS, but whether or not you think there is utility in mathematics without mechanised tools, it doesn't change the fact that TLA+ is formalised mathematics.

> From my perspective this reduces a TLA+ program to a piece of writing, since nothing automated can be done with it.

It's not a program, and often times mathematics is "a piece of writing that nothing automated can be done with."

> The interesting TLA+ programs

Not programs, formulas. Again, they cannot be executed, although their veracity could be checked. Here is a TLA+ specification: `3 * 3 = 9`. Here is another one: `∀ x ∈ Nat : x * x ≥ x` [1]. These two can easily be checked to be true, yet they are not programs. Sure, mathematics can (and is) used to describe aspects of the dynamics of a thrown ball or of an algorithm, but that doesn't make mathematics a ball-manufacturing machine nor a programming language. You can use TLA+ to specify the quicksort algorithm and prove that it, indeed, sorts its input, but you don't use it to produce an executable program that sorts a list (unless you use a very limited subset and write a tool that can translate formulas of certain forms to a computer program).

[1]: I'm eliding some details because TLA+ formulas are interpreted in the TLA logic, where formulas have very specific semantics, but it's close enough for our purpose.

[auggierose]

Proving the Riemann hypothesis might also take longer than you live, and in fact may be impossible. So the Riemann hypothesis is not math?

[RandomThoughts3]

Coq is not a specification language. It’s an interactive theorem prover. The goal set is completely different.

[AlotOfReading]

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]

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]

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]

"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.