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

TLA+ Action Properties

hillelwayne.com

Post reply on HN
Print view View original

11–20 of 38 posts

Re: TLA+ Action Properties

#11

Post by hwayne »

pron wrote: post #7

A very useful article for the non-noob learner of TLA+! > This is the launching point into refinement, or using an entire specification as the checked property of another spec. We use the term "refinement" for those more special cases where `A` and `B` are both canonical formulas (`Init ∧ □[Next]_vars ∧ Fairness`), or, at least, both contain an initial state predicate and at least one box-action clause, but when lear…

It's worth noting that while it's not anything special from a math point of view, there's a lot more technique involved in specifying and verifying `ImplSpec => AbSpec`, which is why it's considered a more advanced topic.

Re: TLA+ Action Properties

#12

Post by hwayne »

pron wrote: post #9
TTPrograms wrote: post #8

Earlier quoted context omitted.

Would it make sense for the TLA+ source to just be a subset of LaTeX, then? At least some fraction of the potential userbase is already familiar with that.

It largely already is. E.g. you can write \forall rather than \A, \lor instead of \/, \neg instead of ~, etc.. The representation most people choose to write as their ASCII typesetting source is just more ergonomic, as it's specifically tailored for TLA+; conversely, there is a LaTeX mode that renders TLA+. Anyway, it's not what you're supposed to read . The vast majority of TLA+ is readable to someone familiar with…

This messes me up when I'm writing actual LaTeX because I keep writing `\A` instead of `\forall`

EDIT: Also that spec uses a lot of really interesting techniques, such that doing a breakdown would be a good Blub study. Off to the typewriter!

Re: TLA+ Action Properties

#14

Post by Jtsummers »

codingforprod wrote: post #13

How should I get started with TLA+? I don’t have any experience.

hwayne's Learn TLA+ [0] is a very approachable introduction and survey. Lamport's TLA+ course [1] is an excellent follow on after going through Hillel's course. That link also includes the book itself.

[0] https://learntla.com/introduction/

[1] https://lamport.azurewebsites.net/tla/learning.html

Re: TLA+ Action Properties

#15

Post by elcapitan »

hwayne wrote: post #10
gambler wrote: post #2

[][x' > x]_x TLA+ seems like an incredibly useful tool, but damn it could do with a better syntax. Math notation is designed to be written on paper and to handle extreme repetitiveness when you do proofs or calculations. Both of those premises are largely irrelevant in the domain TLA+ is intended for.

We're seeing more people create DSLs that compile to TLA+. For example, salt lets you write TLA+ specs in Clojure: https://github.com/Viasat/salt

That's interesting, are there more examples of such languages?

Re: TLA+ Action Properties

#16

Post by lakecresva »

pron wrote: post #6
gambler wrote: post #2

[][x' > x]_x TLA+ seems like an incredibly useful tool, but damn it could do with a better syntax. Math notation is designed to be written on paper and to handle extreme repetitiveness when you do proofs or calculations. Both of those premises are largely irrelevant in the domain TLA+ is intended for.

First, what you posted (and the article uses), is not really TLA+ syntax, but its ASCII source; it's like publishing the LaTeX source for your typeset maths. TLA+ syntax looks like what you see here: https://pron.github.io/posts/tlaplus_part2 Some TLA+ bloggers publish the typesetting source rather than actual pretty-printed TLA+; I'm not thrilled with that, but there's a good, mundane, reason for doing it: there is…

I think you'll be more successful as an advocate for TLA+ if you just say "yeah, the syntax isn't for everyone", or "the tooling has some issues" instead of writing long missives about how syntax like `[][x' /= x => y' = x]_>` is actually motivated by some deep mathematical insight, or suggesting that the desire for an editing environment that doesn't feel 20 years old stems from a failure to understand the difference between specification and programming.

Re: TLA+ Action Properties

#17

Post by pron »

lakecresva wrote: post #16
pron wrote: post #6

Earlier quoted context omitted.

First, what you posted (and the article uses), is not really TLA+ syntax, but its ASCII source; it's like publishing the LaTeX source for your typeset maths. TLA+ syntax looks like what you see here: https://pron.github.io/posts/tlaplus_part2 Some TLA+ bloggers publish the typesetting source rather than actual pretty-printed TLA+; I'm not thrilled with that, but there's a good, mundane, reason for doing it: there is…

I think you'll be more successful as an advocate for TLA+ if you just say "yeah, the syntax isn't for everyone", or "the tooling has some issues" instead of writing long missives about how syntax like `[][x' /= x => y' = x]_ >` is actually motivated by some deep mathematical insight, or suggesting that the desire for an editing environment that doesn't feel 20 years old stems from a failure to understand the differen…

It's not deep mathematical insight, just standard notation, most of this syntax is ~100 years old and already familiar to many; what you wrote is just the typesetting source for: □[x' ≠ x ⇒ y' = x]⟨ₓ,ᵧ⟩ (unicode approximation), much of which is immediately familiar to anyone who reads maths, some of it is standard modal/temporal logic notation [1], and the square brackets and subscript are, indeed a TLA-specific operator; I think writing maths in a less familiar notation would be less appealing and require more training [2]. I did say that the tooling is missing an HTML formatter, which is why some bloggers prefer posting the source rather than the typeset maths. Still, the syntax -- standard mathematical notation -- isn't for everyone, just as Python or Java syntax isn't for everyone, either, and yeah, the tooling has some issues.

Also, yes, it is my opinion that if you focus on an editing environment -- which I like, BTW -- for short mathematical texts that you rarely actually edit compared to most other kinds of texts, then you're missing something quite fundamental about TLA+ (if you don't like the editor, pen and paper is another nice editing environment for TLA+; it's also a standard maths editing environment, but it feels more than 20 years old).

But that's just my opinion, and you don't have to agree with it one bit, just as I don't have to agree with yours. I'm not the boss of TLA+, nor its official ambassador, just someone who likes it, and you should form your own opinions. You really shouldn't take what anyone else you don't personally know says on the internet too seriously. I do like TLA+ a lot, which is why I'm exited to talk about it, but if you like it for completely different reasons or even don't like it at all, that's perfectly fine, too. My enjoyment of TLA+ or practical gain from it isn't harmed by you not liking it. It is fun to talk about something you like with others who like it, too, but if we all liked the same things the world would be pretty boring. Many people dislike the things I like, and sometimes I even like arguing with them. But it's not my mission to get you to like the same things I do.

[1]: That notation is due to https://en.wikipedia.org/wiki/C._I._Lewis#Logic

[2]: E.g. TLA+ functions don't behave like programming language subroutines; using the same syntax might be more familiar, but also more confusing because the text would look the same but mean something different.

Re: TLA+ Action Properties

#18

Post by jacques_chester »

pron wrote: post #17
lakecresva wrote: post #16

Earlier quoted context omitted.

I think you'll be more successful as an advocate for TLA+ if you just say "yeah, the syntax isn't for everyone", or "the tooling has some issues" instead of writing long missives about how syntax like `[][x' /= x => y' = x]_ >` is actually motivated by some deep mathematical insight, or suggesting that the desire for an editing environment that doesn't feel 20 years old stems from a failure to understand the differen…

It's not deep mathematical insight, just standard notation, most of this syntax is ~100 years old and already familiar to many; what you wrote is just the typesetting source for: □[x' ≠ x ⇒ y' = x]⟨ₓ,ᵧ⟩ (unicode approximation), much of which is immediately familiar to anyone who reads maths, some of it is standard modal/temporal logic notation [1], and the square brackets and subscript are, indeed a TLA-specific oper…

> much of which is immediately familiar to anyone who reads maths

Most programmers don't read math. A tool pitched to programmers gains no advantage from being readable primarily by mathematicians.

Re: TLA+ Action Properties

#19

Post by pron »

jacques_chester wrote: post #18
pron wrote: post #17

Earlier quoted context omitted.

It's not deep mathematical insight, just standard notation, most of this syntax is ~100 years old and already familiar to many; what you wrote is just the typesetting source for: □[x' ≠ x ⇒ y' = x]⟨ₓ,ᵧ⟩ (unicode approximation), much of which is immediately familiar to anyone who reads maths, some of it is standard modal/temporal logic notation [1], and the square brackets and subscript are, indeed a TLA-specific oper…

> much of which is immediately familiar to anyone who reads maths Most programmers don't read math. A tool pitched to programmers gains no advantage from being readable primarily by mathematicians.

But that tool is mathematics. As far as I know -- at least, that's what things were like in my time in school -- when programmers learn mathematics they use standard notation, not their own. When they use the tool called natural language to write documentation, they also use standard notation, not their own, and when they study diagrams they (at least I) prefer looking at a pictures with lines rather than SVG source. I don't understand why a tool that is used by programmers but is nothing at all like a computer program should use computer program notation, and I don't think programmers would prefer reading mathematics differently from everyone else.

I believe the reason this comes up in the first place is that people confuse TLA+'s mathematics with programming (or else why would they even ask something so different from programming to look like programming?). There are specification languages that are, or look like, programming languages; TLA+ came later and is intentionally different -- what's different isn't just the notation but the very meaning of the expressions you write. Why is it different? Because mathematics is simpler than even the most basic programming language -- which has such complex notions like a call stack or evaluation order -- and therefore clearer, and clarity is of the utmost importance in specification. I grew to appreciate that a great deal, and I think that decision makes TLA+ both clearer and more powerful than other specification languages. But you are right -- familiarity to programmers isn't one of it's strengths, but it has many others that, in my opinion, more than make up for that.

Re: TLA+ Action Properties

#20

Post by hwayne »

lakecresva wrote: post #16
pron wrote: post #6

Earlier quoted context omitted.

First, what you posted (and the article uses), is not really TLA+ syntax, but its ASCII source; it's like publishing the LaTeX source for your typeset maths. TLA+ syntax looks like what you see here: https://pron.github.io/posts/tlaplus_part2 Some TLA+ bloggers publish the typesetting source rather than actual pretty-printed TLA+; I'm not thrilled with that, but there's a good, mundane, reason for doing it: there is…

I think you'll be more successful as an advocate for TLA+ if you just say "yeah, the syntax isn't for everyone", or "the tooling has some issues" instead of writing long missives about how syntax like `[][x' /= x => y' = x]_ >` is actually motivated by some deep mathematical insight, or suggesting that the desire for an editing environment that doesn't feel 20 years old stems from a failure to understand the differen…

The syntax isn't for everyone and the tooling has some issues.
Post reply on HN