This thread has been going on, let me try to distill the points:
- TLA+ is "definitely not" a programming language (per you and Leslie Lamport).
- TLC has got nothing to do with TLA+ (as a mathematical formalism). TLC is not "an implementation of TLA+". (per you)
- TLC is a tool that can process "something like" TLA+. You say "subset", but it seems to me it is not a strict subset, because special operators like "Print" have different semantics. Let's suggestively call what it processes "TLA-PL". You mention additional configuration but the configuration can be empty so it's really like a pragma or compiler option.
- TLC can evaluate and print TLA-PL expressions in a REPL. (per the repo I linked)
- TLC and TLA-PL could be extended to implement typical programming language primitives such as input, a Java FFI, etc., fairly easily (per observation of the source code)
- TLA-PL is not TLA+, because it is not a rich mathematical formalism, like a drawing tool or English. The purpose of a TLA-PL document ("program") is to produce an output that's either TRUE or a counterexample, although there are other modes of running TLA-PL. In contrast, the purpose of TLA+ is itself, and a TLA+ document ("specification") has no output - the deliverable is the document.
Now it is true that other programs have REPL-like functionality, like the calculator you mention. Generally the benchmark between calculation and programming is Turing completeness, e.g. whether the language can express recursion. In a calculator, if you add a few statements like stack push/pop and command names, suddenly it is a "programmable" calculator like the HP-32S, and Turing complete, and the calculation language becomes a programming language. What about TLA-PL? Naturally TLA-PL expresses recursive statements easily - it is almost trivially Turing complete and hence a programming language. And it is clear by definition that TLC is an interpreter for TLA-PL, so TLA-PL is even an implemented programming language. This is what distinguishes it from the majority of formalisms, in that most formalisms (English, mathematics), although potentially usable for programming, do not have working implementations. It is not a requirement to be a programming language that everything written in the language is computable - Verilog, for example, is actually quite flexible as a hardware synthesis language, allowing one to write unsynthesizable programs, but in practice people simply avoid writing these programs when doing hardware synthesis. Similarly I am sure that valid-looking TLA-PL programs will look correct but nonetheless fail to run under TLC due to limitations of the model checking and so on.
Now it is true that TLC, although it implements TLA-PL, is not an implementation of TLA+, as by definition TLA+ is like mathematics, infinite in scope, hence not implementable. I would argue this also means TLA+ also isn't even definable, but that's a separate issue. Similarly, Leslie Lamport's purpose in creating TLA+ was not (and is not) to create the programming language TLA-PL, even though it exists. This to me is what you're getting stuck on. As a programming language designer, what I care about is TLA-PL. To me it is clear as day that TLA-PL exists as a programming language and and could be turned into a useful one given sufficient effort to modify TLC. In contrast, all I hear from you is "TLA+ this", "TLA+ that", "pay no attention to the working implementation of TLA-PL". But as I said, I don't care about TLA+ - as soon as you say it realizes unrealizable things, you are speaking poetry rather than programming language design. There are tricks like lazy evaluation and so on where a computer represents "unrepresentable" objects symbolically and thus can manipulate them, and from my understanding some of these tricks are implemented in TLC and TLAPS, but it seems clear you are talking about a level beyond this, where a TLA+ specification cannot be evaluated even with symbolic tricks.
I think your question really is, could one design a programming language -- i.e. a language where everything is executable -- inspired by TLA+? The answer to that is absolutely! Someone here mentioned Quint, which is also intended for verification, but works much more like a programming language, and is inspired by TLA (the temporal logic in TLA+). Microsoft Research's P programming language (https://p-org.github.io/P/) could be said to be such a language, and I recall seeing several one-person attempts whose names I can't remember. There are also temporal-logic- based programming languages that precede TLA+, like Esterel (https://en.wikipedia.org/wiki/Esterel).
> as soon as you say it realizes unrealizable things, you are speaking poetry rather than programming language design
No! Because the purpose of TLA+ is not to build executable things but to help design and reason about executable things, and it turns out that being able to describe non-executable things is very useful for that purpose (as I tried to show with the Halts example). The ability of a mathematical specification language like TLA+ to describe unrealisable things is the source of its power to succinctly and clearly specify realisable things, because a description of something is not the thing itself.
It's like saying I'm not interested in mathematics, only the subset that can describe physical things. But it turns out that restricting mathematics to physical things makes it more difficult to work with.
This isn't poetry, just the practical realities of mathematics.
> TLC
I think your focus on TLC is a distraction because even when your TLA+ specification does describe a computable process, TLC doesn't actually run that process (it can be put in a mode that does, but that's actually more confusing here). TLC behaves more like a sophisticated type-checker. Type checkers are extremely useful (and TLC even more so) when reasoning about a computational system, and some clever people have found ways to program them to produce interesting outputs, but that's not really what you have in mind when you think about running a program.
For example, TLC can check and verify in an instant a specification of an uncountably infinite number of executions, each of infinite length, and yet choke on a specification of only a few possible instances of, say, QuickSort.
> it seems clear you are talking about a level beyond this, where a TLA+ specification cannot be evaluated even with symbolic tricks.
Yes, but even that is not the point. You seem to be very focused on execution, programming, and evaluation, and these are not the things that TLA+ helps with.
There is no doubt that a programming language is more useful than a mathematical specification for producing software -- because you can build software without a mathematical specification but not without a program -- just as a hammer is more useful than a blueprint when building a cabin, as you can build the cabin without a blueprint, but not without a hammer. But asking how to fashion the blueprint into a hammer misses its point.
Consider this mathematical description of the vertical motion of a projectile thrown from ground level:
y = v0*t + 0.5gt^2
You can certainly numerically evaluate this formula at different points to create a simulation and plot its motion, and that is very useful, but it's not nearly the only useful thing you can do with the formula. By applying mathematical transformations on the formula (without evaluating it) you can answer questions such as "at what speed should I throw the projectile so that its maximum height exceeds 10m?" or "at what speed should I throw the projectile so that it hits the ground again after exactly 5s?"
The purpose of TLA+ is to write a small specification of the relevant details of a 5MLOC program, and use it to answer questions such as "can network faults lead to a loss of data?" Sure, running the program is the ultimate goal, but being able to answer such questions can be extremely helpful, and is hard to do with a detailed description that's 5 million lines long.
Now, it's perfectly fine to say that you don't care about such capabilities, but these are the capabilities that TLA+ exists to give.
There are languages out there that aim to do both -- produce an executable and offer advanced reasoning capabilities -- but these languages usually turn out to be much more difficult to program with than traditional programming languages and harder to reason with than with TLA+.
> the purpose of TLA+ is to help design and reason about executable things
> execution - [this is not one of] the things that TLA+ helps with.
I think there is a depth limit on HN so I'm just going to stop after this. No, I do not have a "real question". I made a statement, that TLA-PL is a programming language. You still not have agreed or disagreed with this statement, just said that you find it "a distraction" and "confusing" and "not really what you have in mind". Well, un-confuse yourself and present an opinion on its veracity. I don't think it's a distraction because it is a point Lamport brought up in TFA.
> I made a statement, that TLA-PL is a programming language
It is a programming language only the same sense that some subset of English that you could interpret as instructions is a programming language. It's not that you can say, if you only use these symbols then you'd get something executable. While a language could technically be defined like that (a language is just a set of strings), programming languages (and all practical formal languages) are usually defined in a way that it is very easy to mechanically determine whether or not something is in the language and even have a generative grammar for it.
But yes, it is true that are subsets of rich mathematical formalisms (including TLA+) as well as of English that could be "executable", but these subsets are not as easily recognised. So it's a matter of how you define a programming language. If you consider "the subset of English that could be interpreted as a program" to be a programming language, then yes, such subsets of mathematical formalisms including TLA+ exist. If you also require that a programming language is a language that should be easy to decide whether some string is in the language or not, then you'd have to restrict the subset to be very small (just as it is easy to decide the subset of mathematical expressions that can be evaluated by a calculator), and then it's again up to you whether or not you would consider something so rudimentary to be a programming language.
To be more specific, I would not consider the subset of TLA+ that can be simulated or checked by TLC in a way that you'd want an interpreter for a programming language to behave to be a programming language because that subset is not easy to define. For example, you could have two specification of the same program, both of which in the subset that TLC supports, and yet TLC would exhibit a behaviour that could resemble an "execution" for one and not terminate for the other -- even though their meaning is identical. That is because TLC performs a certain analysis of the specification to determine whether some propositions are true or false (e.g. a proposition that a certain variable is always of the same "type") and the algorithm used by that analysis sometimes resembles how people would imagine an interpreter to work and sometimes it doesn't.
So I would say that that subset, like a similar subset of English, is more "a language that could be used to produce a program" than "a programming language" because it is neither as well-defined nor as well-behaved as what we expect from a programming language.
On the other hand, there is an even smaller subset of the language than the one supported by TLC, which could be easily defined, well behaved, and guaranteed to be executable, but it would be quite limited and not make a useful programming language. You can still call it a programming language, but again, it would be smaller than the subset TLC supports.
- TLA+ is "definitely not" a programming language (per you and Leslie Lamport).
- TLC has got nothing to do with TLA+ (as a mathematical formalism). TLC is not "an implementation of TLA+". (per you)
- TLC is a tool that can process "something like" TLA+. You say "subset", but it seems to me it is not a strict subset, because special operators like "Print" have different semantics. Let's suggestively call what it processes "TLA-PL". You mention additional configuration but the configuration can be empty so it's really like a pragma or compiler option.
- TLC can evaluate and print TLA-PL expressions in a REPL. (per the repo I linked)
- TLC and TLA-PL could be extended to implement typical programming language primitives such as input, a Java FFI, etc., fairly easily (per observation of the source code)
- TLA-PL is not TLA+, because it is not a rich mathematical formalism, like a drawing tool or English. The purpose of a TLA-PL document ("program") is to produce an output that's either TRUE or a counterexample, although there are other modes of running TLA-PL. In contrast, the purpose of TLA+ is itself, and a TLA+ document ("specification") has no output - the deliverable is the document.
Now it is true that other programs have REPL-like functionality, like the calculator you mention. Generally the benchmark between calculation and programming is Turing completeness, e.g. whether the language can express recursion. In a calculator, if you add a few statements like stack push/pop and command names, suddenly it is a "programmable" calculator like the HP-32S, and Turing complete, and the calculation language becomes a programming language. What about TLA-PL? Naturally TLA-PL expresses recursive statements easily - it is almost trivially Turing complete and hence a programming language. And it is clear by definition that TLC is an interpreter for TLA-PL, so TLA-PL is even an implemented programming language. This is what distinguishes it from the majority of formalisms, in that most formalisms (English, mathematics), although potentially usable for programming, do not have working implementations. It is not a requirement to be a programming language that everything written in the language is computable - Verilog, for example, is actually quite flexible as a hardware synthesis language, allowing one to write unsynthesizable programs, but in practice people simply avoid writing these programs when doing hardware synthesis. Similarly I am sure that valid-looking TLA-PL programs will look correct but nonetheless fail to run under TLC due to limitations of the model checking and so on.
Now it is true that TLC, although it implements TLA-PL, is not an implementation of TLA+, as by definition TLA+ is like mathematics, infinite in scope, hence not implementable. I would argue this also means TLA+ also isn't even definable, but that's a separate issue. Similarly, Leslie Lamport's purpose in creating TLA+ was not (and is not) to create the programming language TLA-PL, even though it exists. This to me is what you're getting stuck on. As a programming language designer, what I care about is TLA-PL. To me it is clear as day that TLA-PL exists as a programming language and and could be turned into a useful one given sufficient effort to modify TLC. In contrast, all I hear from you is "TLA+ this", "TLA+ that", "pay no attention to the working implementation of TLA-PL". But as I said, I don't care about TLA+ - as soon as you say it realizes unrealizable things, you are speaking poetry rather than programming language design. There are tricks like lazy evaluation and so on where a computer represents "unrepresentable" objects symbolically and thus can manipulate them, and from my understanding some of these tricks are implemented in TLC and TLAPS, but it seems clear you are talking about a level beyond this, where a TLA+ specification cannot be evaluated even with symbolic tricks.