4 ms·

> You can write hello world in TLA+: That's not a good example, but before I get to that, you are again using logical implications in the wrong direction. You

by pron 2y ago

> You can write hello world in TLA+: That's not a good example, but before I get to that, you are again using logical implications in the wrong direction. You can describe physical systems, including programs in mathematics. What makes mathematics not the same as physics or programming is that you can also describe things that aren't physical or computable. It's like you're trying to prove that New York is the United States by pointing out that if you're in NY you're in the US. Let me write that another way: programming ⊊ mathematics. So you can write all programs in mathematics; you cannot do all mathematics in a programming language. Therefore, to know whether TLA+ is programming or mathematics the question is not whether you can describe programs in TLA+ but whether you can describe the maths that isn't programs, and you can. Now, the reason that your example is not good is that the PrintT operator is defined in TLA+ [1] like so: PrintT(x) ≜ TRUE It has no meaning in TLA+ other than the value TRUE. It's just another way of writing TRUE. The computer program TLC, however, prints some output when it encounters the PrintT operator in a specification, but that behaviour is very much not the meaning that operator has in TLA+. TLC can equally print "hello" whenever it encounters the number 3 in a mathematical formula. There are other TLC tricks that can be used to manipulate it to do clever stuff [2], but that's all specific to TLC and not part of the TLA+ language. You could, however, have pointed out that you can specify a Hello, World program in TLA+, only that is unsurprising because you'd specify it in mathematics, and mathematics can also specify a Hello, World program. Here's how I would specify such a program in TLA+ (ignoring liveness for the sake of simplifying things): VARIABLE console Spec ≜ console = "" ∧ □[console' = "Hello, World!"]_console It means that a variable named console (which we'll take to represent the content of the console) starts out blank, and at some future point its content becomes "Hello, World!" and it is not changed further. You could also specify it another way, say, represent the console as a function of time (I'll make it discrete for simplicity): console[t ∈ Nat] ≜ IF t = 0 THEN "" ELSE "Hello, World!" [1]: https://github.com/tlaplus/tlaplus/blob/0dbe98d51d6f05c356303b5e0e7d8ae4a85d144b/tlatools/org.lamport.tlatools/src/tla2sany/StandardModules/TLC.tla#L18 https://github.com/tlaplus/tlaplus/blob/0dbe98d51d6f05c35630... [2]: I've even given a talk about such tricks: https://youtu.be/TP3SY0EUV2A https://youtu.be/TP3SY0EUV2A

Mathnerd314 2y ago
> the PrintT operator is defined in TLA+ like so No, it is defined like so: https://github.com/tlaplus/tlaplus/blob/0dbe98d51d6f05c356303b5e0e7d8ae4a85d144b/tlatools/org.lamport.tlatools/src/tlc2/module/TLC.java#L86 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 2y ago
  > 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 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.

by pron 2y ago

Mathnerd314 2y ago

> the PrintT operator is defined in TLA+ like so No, it is defined like so: https://github.com/tlaplus/tlaplus/blob/0dbe98d51d6f05c356303b5e0e7d8ae4a85d144b/tlatools/org.lamport.tlatools/src/tlc2/module/TLC.java#L86 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 2y ago
> 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 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.