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