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

21–30 of 38 posts

Re: TLA+ Action Properties

#21

Post by gralx »

Jtsummers wrote: post #14
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

I would add an excellent introduction by Scott Wlaschin on YouTube called "Building confidence in concurrent code using a model checker."[0]

Lamport's Specifying Systems (2002, linked above) is a great book. It covers ground quickly but has deep roots - you can tell Lamport is an expert logician who engineered the language carefully. I recommend you read the first two chapters of that (free) book before you do anything else, but you may feel like you're wading through mud if you don't start writing simple specs and watch his or other tutorials by chapter 5. Most of his example specifications (Chapter 5, Chapter 11) design a memory interface for a computer, and they suppose you are familiar with basic computer architecture. If not, you'll have to learn TLA+ while learning how a memory interface works at the same time, which takes dedication.

The appeal to me of TLA+ is using set theory and first-order predicate logic to describe any system, from a poker game to a shopping trip to a computer program - anything at all where the next state depends on the history of the system after a set of initial states. The TLA+ Toolbox IDE has a TLA+ model checker called TLC that can test your logic, and that is particularly useful for a complex concurrent or distributed system if you ever design one.

[0] https://www.youtube.com/watch?v=tqwcz-Yt9gQ

Re: TLA+ Action Properties

#22

Post by michael_j_ward »

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

wow, that feels extremely more approachable.

Are there downsides to using that?

Re: TLA+ Action Properties

#23

Post by hwayne »

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…

It's still a barrier for beginners. I teach both TLA+ and Alloy and people struggle with remembering TLA+ tokens much more than they do with Alloy, which has synonyms for common operators. You can write `implies` instead of `=>` if you want, which makes the teaching experience much smoother. If I could have students use `&&`, `||`, and `!` instead of ⋀ ⋁ ¬ that'd cut out a lot of early friction.

This is also why I "pythonize" the TLA+ tokens during talks. Trying to explain the math syntax gets in the way of explaining the core ideas.

Re: TLA+ Action Properties

#24

Post by hwayne »

michael_j_ward wrote: post #22
hwayne wrote: post #10

Earlier quoted context omitted.

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

wow, that feels extremely more approachable. Are there downsides to using that?

I've never used salt myself so couldn't tell you. From a skim, it looks like they don't have module instantiation? Depending on what you're doing that could be a limitation.

Re: TLA+ Action Properties

#25

Post by hwayne »

elcapitan wrote: post #15
hwayne wrote: post #10

Earlier quoted context omitted.

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?

The other one I know about is PGo, which is a bidirectional go-pluscal compiler: https://github.com/UBC-NSS/pgo

Re: TLA+ Action Properties

#26

Post by barakm »

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.

I've started working on doing TLA+-style models but using Python as the language for doing so (disassembly and all) with an easier to deploy model checker.

Super super early and I'm not quite yet ready to announce it, so don't expect miracles (or post it everywhere) but if you're reading this comment and want to see hacks in this space...

https://github.com/timewinder-dev/timewinder

Re: TLA+ Action Properties

#27

Post by hwayne »

hwayne wrote: post #20
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…

The syntax isn't for everyone and the tooling has some issues.

One of the reasons I'm so bullish on TLA+ is that "the tooling has some issues" is a fixable problem, and the bigger the community, the more likely it is to get fixed.

Re: TLA+ Action Properties

#28

Post by lakecresva »

hwayne wrote: post #20
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…

The syntax isn't for everyone and the tooling has some issues.

Touche.

Re: TLA+ Action Properties

#29

Post by jacques_chester »

pron wrote: post #19
jacques_chester wrote: post #18

Earlier quoted context omitted.

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

So is it for programmers or is it for mathematicians?
Post reply on HN