[HN Gopher] The Future of TLA+ [pdf]
___________________________________________________________________
The Future of TLA+ [pdf]
Author : tkhattra
Score : 113 points
Date : 2024-08-28 18:46 UTC (4 hours ago)
(HTM) web link (lamport.azurewebsites.net)
(TXT) w3m dump (lamport.azurewebsites.net)
| threatofrain wrote:
| A TLA+ alternative people might find curious.
|
| https://quint-lang.org/
| westurner wrote:
| What are other limits and opportunities for TLA+ and similar
| tools?
| max_ wrote:
| Limits of TLA+
|
| - It cannot compile to working code
|
| - Steep learning curve
|
| Opportunities for TLA+
|
| - Helps you understand complex abstractions & systems
| clearly.
|
| - It's extremely effective at communicating the components
| that make up a system with others.
|
| Let get give you a real practical example.
|
| In the AI models there is this component called a
| "Transformer". It under pins ChatGPT (the "T" in ChatGPT).
|
| If you are to read the 2018 Transfomer paper "Attention is
| all you need".
|
| They use human language, diagrams, and mathematics to
| describe their idea.
|
| However if your try to build you own "Transformer" using that
| paper as your only resource your going to struggle
| interpreting what they are saying to get working code.
|
| Even if you get the code working, how sure are you that what
| you have created is EXACTLY what the authors are talking
| about?
|
| English is too verbose, diagrams are open to interpretation &
| mathematics is too ambiguous/abstract. And already written
| code is too dense.
|
| TLA+ is a notation that tends to be used to "specify
| systems".
|
| In TLA+ everything is a defined in terms of a state machine.
| Hardware, software algorithms, consensus algorithms (paxos,
| raft etc).
|
| So why TLA+?
|
| If something is "specified" in TLA+;
|
| - You know exactly what it is -- just by interpreting the
| TLA+ spec
|
| - If you have an idea to communicate. TLA+ literate people
| can understand exactly what your talking about.
|
| - You can find bugs in an algorithms, hardware, proceseses
| just by modeling them in TLA+. So before building Hardware or
| software you can check it's validity & fix flaws in its
| design before committing expensive resources only to
| subsequently find issues in production.
| skybrian wrote:
| Is that a practical example? Has anyone specified a
| transformer using TLA+? More generally, is TLA+ practical
| for code that uses a lot of matrix multiplication?
| drdrey wrote:
| It's really not, TLA+ works best for modeling state
| machines with few discrete states and concurrent systems.
| It can find interesting interleaving of events that would
| leave to a violation of your system properties
| fiddlerwoaroof wrote:
| The most practical examples I'm aware of are the usage of
| TLA+ to specify systems at AWS:
| https://lamport.azurewebsites.net/tla/formal-methods-
| amazon....
| westurner wrote:
| From "Use of Formal Methods at Amazon Web Services"
| (2014) https://lamport.azurewebsites.net/tla/formal-
| methods-amazon.... :
|
| > What Formal Specification Is Not Good For: _We are
| concerned with two major classes of problems with large
| distributed systems: 1) bugs and operator errors that
| cause a departure from the logical intent of the system,
| and 2) surprising 'sustained emergent performance
| degradation' of complex systems that inevitably contain
| feedback loops. We know how to use formal specification
| to find the first class of problems. However, problems in
| the second category can cripple a system even though no
| logic bug is involved. A common example is when a
| momentary slowdown in a server (perhaps due to Java
| garbage collection) causes timeouts to be breached on
| clients, which causes the clients to retry requests,
| which adds more load to the server, which causes further
| slowdown. In such scenarios the system will eventually
| make progress; it is not stuck in a logical deadlock,
| livelock, or other cycle. But from the customer 's
| perspective it is effectively unavailable due to
| sustained unacceptable response times. TLA+ could be used
| to specify an upper bound on response time, as a real-
| time safety property. However, our systems are built on
| infrastructure (disks, operating systems, network) that
| do not support hard real-time scheduling or guarantees,
| so real-time safety properties would not be realistic. We
| build soft real-time systems in which very short periods
| of slow responses are not considered errors. However,
| prolonged severe slowdowns are considered errors. We
| don't yet know of a feasible way to model a real system
| that would enable tools to predict such emergent
| behavior. We use other techniques to mitigate those
| risks._
|
| Delay, cycles, feedback; [complex] [adaptive]
| nonlinearity
|
| Formal methods including TLA+ also can't/don't prevent or
| can only workaround side channels in hardware and
| firmware that is not verified. But that's a different
| layer.
|
| > _This raised a challenge; how to convey the purpose and
| benefits of formal methods to an audience of software
| engineers? Engineers think in terms of debugging rather
| than 'verification', so we called the presentation
| "Debugging Designs" [8] . Continuing that metaphor, we
| have found that software engineers more readily grasp the
| concept and practical value of TLA+ if we dub it:_
| Exhaustively testable pseudo-code
|
| > _We initially avoid the words 'formal', 'verification',
| and 'proof', due to the widespread view that formal
| methods are impractical. We also initially avoid
| mentioning what the acronym 'TLA' stands for, as doing so
| would give an incorrect impression of complexity._
|
| Isn't there a hello world with vector clocks tutorial? A
| simple, formally-verified hello world kernel module with
| each of the potential methods would be demonstrative, but
| then don't you need to model the kernel with abstract
| distributed concurrency primitives too?
|
| From https://news.ycombinator.com/item?id=40980370 ;
|
| > - [ ] DOC: learnxinyminutes for tlaplus
|
| > _TLAplus:https://en.wikipedia.org/wiki/TLA%2B _
|
| > _awesome-tlaplus > Books, (University) courses teaching
| (with) TLA+: https://github.com/tlaplus/awesome-
| tlaplus#books _
|
| FizzBee, Nagini, deal-solver, z3, dafny;
| https://news.ycombinator.com/item?id=39904256#39938759 ,
|
| "Industry forms consortium to drive adoption of Rust in
| safety-critical systems" (2024)
| https://news.ycombinator.com/item?id=40680722
|
| awesome-safety-critical:
| candiddevmike wrote:
| Are there any RFCs written in TLA+?
| koolala wrote:
| Sounds similar to UML: Unified Modeling Language diagrams.
|
| I wonder if TLA+ could convert to diagrams instead of Math
| notation.
| hackermeows wrote:
| you are way off. These is a tool to simulate and validate
| systems and expose edge/race conditions of that system.
| RandomThoughts3 wrote:
| Formal specifications benefits are clear and I think well
| understood at that point. If you want to ensure that your
| specifications is coherent and doesn't have unexpected
| behaviour, having a formal specification is a must. It's even
| a legal requirement for some system nowadays in safety
| critical applications.
|
| The issue of TLA+ is that it doesn't come from the right side
| of the field. Most formal specifications tools were born out
| of necessity from the engineering fields requiring them. TLA+
| is a computer science tool. It sometimes shows in the
| vocabulary used and in the way it is structured.
| lolinder wrote:
| Previously discussed:
| https://news.ycombinator.com/item?id=41111790
| pron wrote:
| I wouldn't say it's a TLA+ alternative because it cannot do the
| most powerful and useful things TLA+ does (esp. refinement),
| but it is an alternative for programmers who just want to
| specify at a level that closer to code and model-check
| specifications.
| hwayne wrote:
| Every time I see a new TLA+ replacement my first thought is
| "Oooh this will be good for the 99% of normal stuff people do
| with TLA+."
|
| Then I look through some of the specs I've written with
| clients and find the one _absolutely insane_ thing I did in
| TLA+ that would be impossible in that replacement.
|
| Shoutout to operator labels.
| bokumo wrote:
| What LaTeX package does one use to get the "back" link at the end
| of footnotes like the linked PDF exhibits?
| gurjeet wrote:
| Yes, that's an interesting implementation. I'm using Firefox,
| and the jumps to the notes and back to the paragraph are
| recorded in history, and has the expected effect when clicking
| the back and forward history arrows/buttons.
| Mathnerd314 wrote:
| > 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 programming
| language to me. A systems programming language, even.
|
| All this is to say that it seems TLA+ really has no future. If
| there was a future, like a goal or a roadmap or something, it
| would be outlined in this document a lot more clearly - whereas,
| instead, it is more like "nope, everything's good, no changes
| needed", even as the language appears nowhere on the TIOBE
| rankings.
| colanderman wrote:
| TLA+ is only "executable" in the same sense that an algebraic
| expression is executable. It's perfectly possible to write
| things on TLA+ that can not be simply executed linearly. (These
| overlap to a great extent with the things which TLC rejects.)
| As a basic example, it's easy to write a statement with \A
| (unbounded universal quantification) whose truth can only be
| judged by a proof engine.
|
| Specification languages are _explicitly not_ programming
| languages, for the core reason that programming languages
| dictate only what _must_ occur; whereas specification languages
| can dictate what must _not_ occur. It 's not possible with a
| "specification" written using a programming language to
| determine what of a program is _actually_ the specification,
| vs. what is an accident of the implementation.
| AlotOfReading wrote:
| Being able to create systems by writing specifications and
| having the computer figure out how to execute them was
| basically the point of fifth generation programming
| languages.
|
| More relevant today, you can execute other "specification"
| languages like Coq and Idris because they support things
| outside the narrow feature set of specification usecases.
|
| TLA+ isn't executable and doesn't look like an imperative
| language because the authors don't want it to be, not because
| there's some universal line dividing specification languages
| from programming languages. It's also one of the biggest
| hurdles to TLA+ usage.
| RandomThoughts3 wrote:
| Coq is not a specification language. It's an interactive
| theorem prover. The goal set is completely different.
| AlotOfReading wrote:
| 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.
| RandomThoughts3 wrote:
| 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 want to. It still remains an interactive prover.
| pron wrote:
| > Being able to create systems by writing specifications
| and having the computer figure out how to execute them was
| basically the point of fifth generation programming
| languages.
|
| Yeah, but in maths you can specify anything, including
| things that the computer is unlikely to figure out how to
| execute if it's possible at all. Programming languages of
| every generation are very useful, as is mathematics, even
| though they're not the same thing.
|
| > More relevant today, you can execute other
| "specification" languages like Coq and Idris because they
| support things outside the narrow feature set of
| specification usecases.
|
| Coq and Idris are very different in the way they're
| typically used, and I'd say TLA+ is much closer to Coq than
| to Idris (and is probably more popular than the two
| combined), but to "execute" anything the specification
| needs to be at a certain level that's detailed enough to
| produce a program, and oftentimes that is very much not
| what you want.
|
| It would be extremely useful to have a language that you
| could describe the various properties of a car and it would
| compile your specification into the design of a car (you
| would need to give it sufficient detail as there are
| choices to be made). But it would also be extremely useful
| to have a language that could be used to learn certain
| things about a car -- say, it's braking distance -- without
| specifying it in sufficient detail to actually build one.
| That is what maths is good for -- describing things at
| _arbitrary_ levels of detail to answer relevant questions.
|
| For example, you may have a 5 MLOC distributed system, and
| you want to know if a certain kind of failure may lead to
| data loss. You could use TLA+ to describe just the relevant
| details to answer the question in, say, 200 lines of
| formulas. That you cannot compile those formulas into a
| working 5 MLOC piece of software is not a downside of
| mathematics, but rather the point.
|
| > TLA+ isn't executable and doesn't look like an imperative
| language because the authors don't want it to be
|
| And because it's not a language for programming but a
| language for mathematics, so it looks and feels pretty
| close to plain mathematics (only it's formal), as that's
| the obvious choice for writing mathematics.
| tailrecursion wrote:
| > "specification of system behavior" sounds like a programming
| language to me. A systems programming language, even.
|
| Lamport has directly and repeatedly addressed the differences
| between what's desirable in a specification language versus
| what's desirable in a programming language. Understanding the
| difference is vital to writing specifications.
| Certhas wrote:
| Simple =/= easy.
|
| It seems to me that TLA+ is executable in the sense that a
| difference equation can be run forward in time. Plenty of
| mathematics is executable in that sense.
|
| Specification is not the same thing as implementation. A
| specification language does not tell a machine what operations
| to perform, a programming language does.
|
| System behavior and systems programming are entirely different
| uses of the word system.
| lolinder wrote:
| > even as the language appears nowhere on the TIOBE rankings.
|
| TIOBE rankings are widely considered to be useless by those who
| care about programming languages, but even aside from that your
| dismissal on those grounds is absurd given that you had just
| barely criticized TLA+ for trying to duck the label of
| "programming language" at all. You can't criticize it for
| trying not to be a programming language and then turn around
| and criticize it for not showing up on a ranking of programming
| languages.
|
| It's excluded from the TIOBE index in the same way that HTML,
| CSS, or Markdown are excluded, and _that 's by choice_.
| hwayne wrote:
| Also, being popular is not the same as being useful.
| Mathematica and Verilog aren't on the TIOBE either, and
| Verilog is a lot more important to society than Logo!
| klingoff wrote:
| > 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?
| pron wrote:
| > 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 wrote:
| > 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
|
| [2] https://mathworld.wolfram.com/ZeroFunction.html
| pron wrote:
| I mean the zero function, i.e., the one that is zero
| everywhere, because if y [?] Z and y = -y, then y = 0.
| foysavas wrote:
| > "specification of system behavior" sounds like a programming
| language to me
|
| By "specification language" Lamport means one capable of
| verification via model checking.
|
| In contrast, "programming languages" are not capable of such
| verification.
| wizerno wrote:
| As someone who's fascinated by formal verification and who's
| early in their career, what advice do senior folks who have been
| using TLA+ have?
|
| TLA+ isn't taught in most universities and while I've read about
| so many interesting applications, I'm yet to convince myself that
| someone would hire me for knowing it rather than just teaching it
| to me on the job. Any tips to get started would also be
| appreciated!
| kadoban wrote:
| 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.
| hwayne wrote:
| > The [\EE] operator is needed to explain the theory underlying
| how TLA+ is used.
|
| There's another reason to potentially support \EE: it's needed to
| refine specs with auxiliary variables. Currently, if an abstract
| spec has `aux_hist` to prove a property or something, you _need_
| the refinement to have an `aux_hist` equivalent, even if it doesn
| 't affect the spec behavior at all. But if checkers could handle
| `\EE` you could instead leave it out of the refinement and check
| `\EE aux_hist: Abstract(aux_hist)!Spec`.
|
| I think /u/pron once told me that _actually checking_ a property
| of that form is 2-EXPTIME complete, though. Which is why it 's
| not supported in practice.
___________________________________________________________________
(page generated 2024-08-28 23:00 UTC)