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.