Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

The Future of TLA+ [pdf]

lamport.azurewebsites.net

Post reply on HN
Print view View original

61–70 of 107 posts

Re: The Future of TLA+ [pdf]

#61

Post by d0mine »

klingoff wrote: post #19
Mathnerd314 wrote: post #9

> Simplicity is a major goal of TLA+. Is TLA+ simple? I find this hard to accept. > TLA+ isn’t a programming language; it’s mathematics. Mathematics is not executable, though, whereas TLA+ is. > TLA+ [is better] for its purpose than a programming language. "TLA+ is a formal specification language designed by Leslie Lamport for the specification of system behavior." "specification of system behavior" sounds like a pro…

> If there was a future, like a goal or a roadmap or something, it would be outlined Where is the outline for English? French has a more structured oversight with organizations and goals, so it will beat English?

It is harder to create/merge numerous dialects for a computer language such as TLA+ than English.

Even the most popular languages such as Python have just a few viable implementations.

Roadmap/focus is useful in a collaboration.

Re: The Future of TLA+ [pdf]

#62

Post by auggierose »

RandomThoughts3 wrote: post #27
AlotOfReading wrote: post #26

Earlier quoted context omitted.

Coq, specifically Gallina, is absolutely a specification tool. It's not only that, but it's one of the big use cases it's explicitly designed to support.

No, it’s not. Gallina is not a specification tool in the way TLA+ is (even if coq calls it its specification language). Gallina is a language used to write mathematical statements which you intend to prove. It’s not designed to write specifications. Coq is definitely not a specification tool. You can probably prove a specification with it in the same way you actually can do symbolic manipulation with C if you really…

Of course Coq is also a specification tool. C compilers have been formally verified with Coq. So you have a spec for C in Coq.

Re: The Future of TLA+ [pdf]

#63

Post by auggierose »

zekrioca wrote: post #56
Jtsummers wrote: post #53

Earlier quoted context omitted.

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

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

This was just an example that TLA+ is not executable.

You didn't realise that f[x] = -f[x] implies f[x] = 0, and that is how it is often: You have some property, but you don't know what it entails exactly. TLA+ allows you to reason about that.

Re: The Future of TLA+ [pdf]

#64

Post by pistoleer »

erichocean wrote: post #48
Mathnerd314 wrote: post #45

Earlier quoted context omitted.

TLA+ is executable in the sense of Prolog: there is an algorithm (the TLA+ implementation) that takes a TLA+ program and produces output. Most mathematics is not executable in this sense, you will have a very difficult time doing anything useful with the PDF's of published math papers. Math is a natural language, TLA+ is not. And I would agree, TLA+ as a specification is different from TLA+ as an implementation. I ge…

> Math is a natural language Almost spit out my drink dude, no jokes this early in the day.

What's the joke?

Re: The Future of TLA+ [pdf]

#65

Post by pistoleer »

pron wrote: post #24
Mathnerd314 wrote: post #9

> Simplicity is a major goal of TLA+. Is TLA+ simple? I find this hard to accept. > TLA+ isn’t a programming language; it’s mathematics. Mathematics is not executable, though, whereas TLA+ is. > TLA+ [is better] for its purpose than a programming language. "TLA+ is a formal specification language designed by Leslie Lamport for the specification of system behavior." "specification of system behavior" sounds like a pro…

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

Ah yes "f triangle equals CHOOSE f member of array of int to int, namely, upside down A x member of int, namely, x'th element of f equals the negative of x'th element of f." Easier than python indeed, where this simple and elegant expression is turned into the much more complicated and ugly form of

    def f(x):
        return -x

Re: The Future of TLA+ [pdf]

#67

Post by bvrmn »

pistoleer wrote: post #65
pron wrote: post #24

Earlier quoted context omitted.

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

Ah yes "f triangle equals CHOOSE f member of array of int to int, namely, upside down A x member of int, namely, x'th element of f equals the negative of x'th element of f." Easier than python indeed, where this simple and elegant expression is turned into the much more complicated and ugly form of def f(x): return -x

You could say you ignored math classes in a more short form. Parent describes a selection of element (f) from a set of functions such that `f(x)` equals `-f(x)`. Your python example is quite far from that.

Re: The Future of TLA+ [pdf]

#68

Post by pistoleer »

bvrmn wrote: post #67
pistoleer wrote: post #65

Earlier quoted context omitted.

Ah yes "f triangle equals CHOOSE f member of array of int to int, namely, upside down A x member of int, namely, x'th element of f equals the negative of x'th element of f." Easier than python indeed, where this simple and elegant expression is turned into the much more complicated and ugly form of def f(x): return -x

You could say you ignored math classes in a more short form. Parent describes a selection of element (f) from a set of functions such that `f(x)` equals `-f(x)`. Your python example is quite far from that.

If a projects desires a future, it requires adoption. For that, it must be approachable. When the syntax throws unicode math symbols at the user, and requires the user to first define the universe before even thinking about "this function negates the input", and in general throws years of programming language syntax conventions away, it's just not approachable.

I understand and empathize with the ideal that everyone should just know college level math. It may even be fun to engage in putting down those who don't. Oh, how they just ignored their classes! Stupid fools!

However, it's not a realistic expectation, even in the field of programming, where a large majority have not been accredited with a math bachelors degree. A LOT of programmers didn't even have computer science formal education.

Meet people where they are and all that. Taking position in an ivory tower allows you to feel intellectually superior, but practically speaking it doesn't actually get you anywhere.

The TLA+ community can not have it both ways, either stop bemoaning the lack of adoption of formal verification, or adapt to meet people where they are at. And certainly don't make redditor-esque proclamations about "just" "simply". Take a step back and think about your goals when you write in such a tone. Are you trying to build something and invite others? Or are you trying to prove your own intellect? To whom and what for?

Re: The Future of TLA+ [pdf]

#69

Post by bvrmn »

pistoleer wrote: post #68
bvrmn wrote: post #67

Earlier quoted context omitted.

You could say you ignored math classes in a more short form. Parent describes a selection of element (f) from a set of functions such that `f(x)` equals `-f(x)`. Your python example is quite far from that.

If a projects desires a future, it requires adoption. For that, it must be approachable. When the syntax throws unicode math symbols at the user, and requires the user to first define the universe before even thinking about "this function negates the input", and in general throws years of programming language syntax conventions away, it's just not approachable. I understand and empathize with the ideal that everyone…

Man. I completely understand your frustration. It's similar how music-illiterate people whine about standard music notation. The math notation in question is literally 30min intro to a set theory. There is no knowledge gate and towers to conquer. Been there and the real ultimate answer: it's a matter of spending a little time and learn stuff.

Re: The Future of TLA+ [pdf]

#70

Post by Turfie »

mnk47 wrote: post #59
kadoban wrote: post #32

Earlier quoted context omitted.

There's very little tech that somebody is going to hire you for knowing. It's a tool like many others. If nothing else, spending a few days playing with it will give you an idea of what it's good for and if you want to continue, or it'll make it stick in your mind so you can come back to it if you ever need it.

>There's very little tech that somebody is going to hire you for knowing. It's a tool like many others. I guess this must be true on places like SF since I see this so often on HN, but almost every single job listing I've seen strictly requires knowledge of a specific tech stack, with the exception of a few internship programs.

Exactly my thoughts as well.
Post reply on HN