3 ms·
> Is TLA+ simple? I find this hard to accept. It is very, very simple, and I would say easier to learn than Python, as long as you remember that it is not prog
by pron 2y ago
> Is TLA+ simple? I find this hard to accept.
It is very, very simple, and I would say easier to learn than Python, as long as you remember that it is not programming but maths. For example, suppose you specify this function on the integers:
f ≜ CHOOSE f ∈ [Int → Int] :
∀ x ∈ Int : f[x] = -f[x]
What function is it? Clearly, it's the zero function rather than what defining the equivalent "programming function" in, say, Haskell would mean:
f :: Integer -> Integer
f x = -(f x)
> Mathematics is not executable, though, whereas TLA+ is.
It is definitely not executable (i.e. not any more than mathematics is; you can specify executable things in maths and therefore in TLA+, but not everything you specify is executable). You can specify non-computable things (e.g. it is trivial to specify a halting oracle) as well as things involving real numbers. Moreover, when you check a TLA+ specification with a model-checker like TLC, it doesn't actually execute the specification, as it can check a specification of uncountable many executions, each of infinite length in a second.
However, you can certainly write formulas specifying the behaviour of an executable program and simulate it with TLC. But this is because you can use mathematics to describe physical systems, but not everything you can describe in mathematics can have a physical representation.
> "specification of system behavior" sounds like a programming language to me. A systems programming language, even.
A program is, indeed, one way of specifying a system, and TLA+ does allow you to specify an algorithm in this way (because maths allows you to specify programs), but it also allows you to specify systems in very useful ways that are very much not programs. For example, you can specify a component that sorts things without ever writing an algorithm for sorting, which is useful when the details of the sorting algorithm are irrelevant to the questions you want to answer. It's like how you can write a formula that treats planets as point-masses if you're interested in orbital mechanics, yet specify the earth in a much more detailed way if you're interested in predicting the weather.
> even as the language appears nowhere on the TIOBE rankings.
It is not a programming language. While it is true that far more people write programs than use mathematics to reason about physics, biology, or the way software systems behave (especially complicated interactive and distributed systems, which is where TLA+ excels), that doesn't mean such disciplines have no future.
- zekrioca 2y ago> It is very, very simple, and I would say easier to learn than Python, as long as you remember that it is not programming but maths. For example, suppose you specify this function on the integers: > f ≜ CHOOSE f ∈ [Int → Int] : > ∀ x ∈ Int : f[x] = -f[x] > What function is it? Clearly, it's the zero function Did you mean your example is the constant function [1], rather than a zero function [2] (where c = 0)? [1] https://mathworld.wolfram.com/ConstantFunction.html https://mathworld.wolfram.com/ConstantFunction.html [2] https://mathworld.wolfram.com/ZeroFunction.html https://mathworld.wolfram.com/ZeroFunction.html
- pron 2y agoI mean the zero function, i.e., the one that is zero everywhere, because if y ∈ ℤ and y = -y, then y = 0.
- zekrioca 2y agoDoesn't ℤ include negative natural numbers? * Nevermind, I just saw you used the ">" sign in the definition. Is it why the definition only applies to positive numbers? In any case, you did not write it in your textual description, which looked confusing to me. I think it would be easier if one could define it as ℤ+ or something like that.
- Jtsummers 2y agoThe original from pron: f ≜ CHOOSE f ∈ [Int → Int] : ∀ x ∈ Int : f[x] = -f[x] You added the > in your quote of pron, he didn't have it in the original. There is no c in ℤ with c != 0 s.t. f(x) = c and f(x) = -f(x), that would imply that c = -c for non-zero integers which is not true. The only function that can satisfy pron's constraints is f(x) = 0 since c = 0 is the only time c = -c, or 0 = -0.
- zekrioca 2y agoThat’s true, my mistake. Thank you for the clarification! In this case, I have another question. Why is this original definition different than say f ≜ CHOOSE f ∈ [Int → Int]: ∀ x ∈ Int : f[x] = 0 If you want some function to be 0, just specify it. Why does one need to find this a broader but more complex way of specifying the possible “input” space in TLA+? How does it help is my question, I guess.