[Mathnerd314]

> the PrintT operator is defined in TLA+ like so

No, it is defined like so: https://github.com/tlaplus/tlaplus/blob/0dbe98d51d6f05c35630... This is the same strategy that Haskell uses for its primops, a placeholder file and implementation in another language. I guess you didn't understand my point that it would be easy to extend TLA+/TLC to more primops, like memory, a Java FFI, and so on, making it a fully featured programming language. I don't care what "the TLA+ language" is, C++ implementers regularly toss the spec in the dumpster and just like you have C++/LLVM and C++/GCC there similarly is a dialect of TLA+ for each implementation.

[pron]

> No, it is defined like so

No, you are looking at the TLC source code, not TLA+ definitions. If you read the TLC documentation, it makes it very clear that it is not TLA+, but a software tool for model checking a certain subset of TLA+ and has some programming-like features that are not in TLA+. Other TLA+ tools also focus on other TLA+ subsets and have their own features, and they're not necessarily consistent with one another.

> This is the same strategy that Haskell uses for its primops

It really isn't, because TLC isn't the TLA+ compiler/interpreter. In TLA+ PrintT is just synonym for TRUE. We can talk about TLC if you like, but you shouldn't confuse the two.

> I guess you didn't understand my point that it would be easy to extend TLA+/TLC to more primops

TLA+ and TLC are two different things. TLA+ is a formal language for writing mathematical specifications. TLC is one of the several tools for analysing TLA+ specifications written in a subset of TLA+.

> I don't care what "the TLA+ language" is

That would sort-of made sense if TLC was the canonical tool for analysing TLA+ but it isn't (certainly not in the sense that ghc is the canonical Haskell compiler). In SANY, TLAPS, and Apalache (another TLA+ model checker), PrintT is just TRUE. In our work on the TLA+ toolbox, we're always careful to separate what's TLA+ and what are the features of the software tools, and in the materials we produce about TLA+ and the TLA+ tools these differences are explained.

In other words, you -- as someone who doesn't know TLA+ -- may not care about what TLA+ is and what TLC is, but those who use TLA+ very much care (though maybe not in the first week), because that distinction is required to put the language to good use.

If you choose to learn TLA+, I'm confident you'll come to agree. Everything I've said here will become clear once learn TLA+, TLC, and TLAPS (or even just TLA+). Those who actually use TLA+ very much do care what "the TLA+ language" is and what are some TLC features, because they often want to use multiple tools to do different things with their specifications, and PrintT only prints stuff when you're using TLC, not, say, when you're using TLAPS or Apalache. Once you gain experience with TLA+ you understand which subset of it can be checked by TLC and which isn't, and you write certain specifications with the intent of checking them in TLC and others for other uses, as you know that they fall outside TLC's subset of TLA+.

I think this short talk I gave and I linked to before (https://www.youtube.com/watch?v=TP3SY0EUV2A) gives a sense of the different ways you use TLA+ and how you combine them. It shows how you use the language as you do ordinary maths -- by manipulating formulas on paper -- and then use the results in conjunction with TLC to obtain some particular kind of automation. In fact, it is about how to use TLA+ to rewrite some TLA+ specifications so that they could be checked in some interesting way by TLC, i.e. the whole premise is that TLA+ users are confronted by the differences between TLC and TLA+, and it shows how to use certain deductions in practice to put TLC into some interesting uses for kinds of TLA+ specifications that TLA+ users would normally think fall outside the bounds of TLC. Anyway, anyone who actually uses TLA+ is -- and needs to be -- very much aware of the differences between TLA+ and TLC, recognises their different roles.

[Mathnerd314]

> If you read the TLC documentation, it makes it very clear that it is not TLA+.

Fine, clearly you are missing the point I am making about how languages become confused with implementations. Just s/TLA+/TLC/ in all the above. Is TLC a programming language implementation or not? Consider for example https://github.com/will62794/tlaplus_repl which evaluates TLC expressions. At what point is there sufficient programming language functionality for you to become convinced that TLC is a programming language?

[pron]

TL;DR: Of course TLA+ can be used to describe all programs, as can all sufficiently-rich mathematical formalisms (regardless of TLC; TLC has got nothing to do with that). It is definitely not a programming language because its expressive power comes from its ability to describe things that cannot be computed (or practically computed). I.e. it's not a programming language not because it's too small of a subset of programming, but rather a vastly larger superset of programming. In other words, TLA+ (and mathematics in general) is not a programming language not because it is less than a programming language but because it is more. If TLA+ is a programming language, then so is any rich mathematical formalism, any drawing tool, or English for that matter.

> Is TLC a programming language implementation or not?

Ok, so first of all, TLC is not "an implementation of TLA+" and not because it can only check a limited subset of TLA+.

To sho that, let me take a short but important detour. What is the purpose of a computer program? It is to produce an output, either for yourself or for others you give the program to. In contrast, what is the purpose of a TLA+ specification, i.e. what is it that you do with it, or what is the deliverable? Clearly, it's not some output because a TLA+ specification has no output (I'll get back to TLC in a moment). Once you're convinced that the TLA+ specification fulfils the propositions you're interested in -- either by inspection, formal manipulation and proof on paper, formal proof checked by TLAPS, or a successful run of TLC -- the deliverable is the TLA+ specification itself, the set of formulas, whose purpose is then for someone (maybe yourself or someone else) to use as a design for some system to build -- a program, a computer chip etc.. So a the purpose and deliverable of a TLA+ specification is it itself, just like the purpose of an architectural blueprint.

Now, back to TLC. TLC is, no doubt, a program that takes as an input a TLA+ specification written in a particular subset of TLA+ and some additional configuration that defines the boundaries of state space to model-check, and produces an output that's either TRUE or a counterexample. There are other modes of running TLC, as well, for which special operators like PrintT can be useful.

Note that there are many other programs that do something with a piece of mathematics and produce an answer. The simplest one is a calculator. A calculator is a program that takes as an input some portion of a mathematical statement in a small subset of mathematics (arithmetic on some finite subset of integers and rationals) and produces an output.

So we can take a partial mathematical statement 3 + 4 and use it, in conjunction with a calculator, as a program that produces the output 7.

So finally, we can answer your question. TLC is a program that's more sophisticated than ordinary calculators, and we can certainly write some mathematical statements in a subset of TLA+ so that when we feed them into TLC we create some interesting output. It is similar to a CAD/CAM tool you run on an architectural blueprint. But is the tool "an implementation" of the blueprint? I don't think that makes sense.

> At what point is there sufficient programming language functionality for you to become convinced that TLC is a programming language?

TLC is not a language but a tool that can process a subset of TLA+. The existence of calculators or of TLC does not mean that mathematics is a programming language, because:

1. Even though mathematics can be used to describe all programs and all of physics -- because the domain describable by mathematics, and therefore by TLA+ -- is a superset of all the behaviours of physical and computable things, it is also a strict superset, and mathematics (and therefore TLA+) can describe lots and lots of things that cannot possibly be realised by anything in the physical world or by any computation.

2. Even though some subset of mathematics (and therefore of TLA+) can be used in conjunction with some program to produce an intended output, that output is not the purpose of mathematics (and therefore of TLA+).

As for 1, you may then ask what's the point of a language that is ultimately intended to produce designs for physically-realisable systems to encompass all of mathematics and describe things that are not realisable. There are two answers to that: first, it makes the working with the language much simpler, just as working in classical mathematics is simpler than working in constructive mathematics (which is based on intuitionistic or some other constructive logic rather than classical logic). Second (and this is really an application of the first answer), specifying non-realisable things is helpful when specifying properties of realisable things. For example, suppose you design an algorithm that can decide whether some specific subset of programs halt. You want to check the proposition that:

    InMySubset(InputProgram) ⇒ MyAlgorithm(InputProgram) = Halts(InputProgram)

and to do that you need to describe the operator Halts even though it is not realisable (as it's not computable). So Halts clearly cannot be written as a program, yet defining it in some mathematical formalism is needed to express a real property of a real program. (BTW, the definition of a Halts operator is a trivial one-liner in TLA+ [1]).

I see that again and again you're getting stuck on the point that because there are programs that can evaluate mathematical statements, mathematics is a programming language. But the fact that you can describe any program or any physical system in mathematics is the point and power of mathematics. But mathematics is neither physics nor programming because it can also describe things outside the world of programs and physics.

Of course you can write programs in every rich mathematical formalism, including TLA+ (and TLC has nothing to do with it; this would be true even if TLC didn't exist). But programming languages are languages that can describe things that live in a small subset of the world of mathematics. TLA+ is not a programming language not because it doesn't contain the universe of all programs -- it does; every imaginable program could be specified in mathematics and specifically in TLA+ -- but because it contains much, much more.

So if you want to define "a programming language" as any language in which you could describe many or perhaps even all computations, then every rich mathematical formalism (and therefore TLA+) could be considered a programming language. But I would think that a language where most things you write are not computable isn't a programming language. Rather, a programming language is one where everything you write in the language is at the very least computable, and that is certainly not the case for TLA+.

Something similar is true for English. You can use English to describe any conceivable algorithm, and there are now tools that could convert a subset of such descriptions to executable software. But the fact you can use English to describe programs doesn't make English a programming language, because many of the things it is used to described aren't programs.

But even if you insist that mathematics (or English) is a programming language, the point is still that mathematics (and TLA+) exists to describe useful things that go well beyond what could be described in a programming language [1].

[1]: Halts(Program, vars) ≜ Program ⇒ ⬦□(vars' = vars)

[2]: I'm overlooking the type level in programming languages with rich type systems (like Agda), but the point still stands, only the details are more technical.

[Mathnerd314]

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.

[pron]

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

[Mathnerd314]

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

[pron]

(Sorry, the + should be a - in the formula above)