[HN Gopher] TLA+ Action Properties
___________________________________________________________________
TLA+ Action Properties
Author : ingve
Score : 73 points
Date : 2021-03-31 16:28 UTC (6 hours ago)
(HTM) web link (www.hillelwayne.com)
(TXT) w3m dump (www.hillelwayne.com)
| codingforprod wrote:
| How should I get started with TLA+? I don't have any experience.
| Jtsummers wrote:
| 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
| gralx wrote:
| 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
| ExcavateGrandMa wrote:
| I wanna die... WTH this undigest stuff :D unmaintanable, awfully
| gambler wrote:
| [][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.
| Jtsummers wrote:
| That's what PlusCal seems to be there to help with. It will
| generate statements like the above from a more Pascal-ish form.
| hwayne wrote:
| 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
| michael_j_ward wrote:
| wow, that feels extremely more approachable.
|
| Are there downsides to using that?
| hwayne wrote:
| 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.
| elcapitan wrote:
| That's interesting, are there more examples of such
| languages?
| hwayne wrote:
| The other one I know about is PGo, which is a bidirectional
| go-pluscal compiler: https://github.com/UBC-NSS/pgo
| pron wrote:
| 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 no
| convenient formatter for HTML yet, only PDF.
|
| Second, TLA+ is very much designed for writing mathematical
| specifications that are much smaller than most programs (a TLA+
| specification with ~2000 lines of maths is _very_ big, while a
| program with 2000 lines of code is quite small), that are then
| read and contemplated _a lot_. Several hours of thought for
| every line of maths is pretty normal for TLA+. Writing maths
| [1] is absolutely not like programming, both for ergonomic and
| workflow reasons (https://old.reddit.com/r/tlaplus/comments/edq
| f6j/an_interest...) as well as semantic reasons (https://old.re
| ddit.com/r/tlaplus/comments/enencr/yet_another...). Easily the
| hardest thing in learning TLA+ (which is a tiny, and extremely
| simple formal maths language) is understanding the difference
| between programming and simple mathematics, and it takes work
| to internalise that. The syntax, which is pretty much standard
| mathematical notation, more or less, helps.
|
| [1]: TLA+ is roughly the discrete analogue to ODEs describing a
| continuous engineered system.
| hwayne wrote:
| 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.
| TTPrograms wrote:
| 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.
| pron wrote:
| 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
| ordinary mathematical notation within two to ten minutes of
| training (if you know temporal logic, then almost all of
| TLA+ is readable within minutes). See e.g. this complete
| (and very sophisticated in its use of advanced TLA+)
| specification, written at Arm, of CPU speculation side-
| channels: http://www.procode.org/cachespec/ (direct link to
| spec: http://www.procode.org/cachespec/CacheSpecv1.pdf).
| The syntax is quite beautiful, and almost immediately
| familiar to anyone who knows standard mathematical
| notation.
| hwayne wrote:
| 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!
| lakecresva wrote:
| 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]_<<x, y>>` 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.
| pron wrote:
| 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.
| jacques_chester wrote:
| > _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.
| pron wrote:
| 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.
| jacques_chester wrote:
| So is it for programmers or is it for mathematicians?
| hwayne wrote:
| The syntax isn't for everyone and the tooling has some
| issues.
| lakecresva wrote:
| Touche.
| hwayne wrote:
| 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.
| _alex_ wrote:
| most of the time I need to read it, I use the PDF generation.
| It turns all the ascii into math symbols. way easier to read
| barakm wrote:
| 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
| pron wrote:
| 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 learning,
| it's important to understand that there is nothing special about
| refinement in TLA+ from a mathematical point-of-view. Every
| formula in TLA+ describes a class of behaviours. The key general
| point to learn is that TLA+ does not distinguish between
| specifications and properties; they're just classes of behaviours
| that we can call a "system property" or a "system specification"
| based on how we psychologically think of it. The TLA+ formula `A
| = B` means that `A`'s behaviours are contained in `B`'s, and can
| be read as "specification A implements specification B" or
| "specification A satisfies property B" or "property B is an
| abstraction of property A" or "specification B is a
| generalisation of property A." All of these are just words used
| to describe the abstraction/refinement relation that's the very
| core of TLA+. So this _is_ refinement, and `#[A]_vars` is an
| entire TLA+ specification, as is `#P` (it is true that TLC cannot
| check the specification `#(x [?] 1..3)` but it can check the
| equivalent formula `x [?] 1..3 [?] #[x ' [?] 1..3]_x` but that
| doesn't make the simpler formulation any less of a valid and
| complete TLA+ specification of a system).
| hwayne wrote:
| 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.
___________________________________________________________________
(page generated 2021-03-31 23:01 UTC)