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