1. 40

Link is to announcement, actual documentation is here.

  1.  

  2. 4

    My last serious thoughts about formal methods are now more than old enough to drink in the US. You say:

    It’s a simple, powerful formal method whose entire syntax fits in just two pages. You can learn it in a day and be productive in two.

    Can you point to a primer that you consider good on what it means to be productive wrt a formal method, why it might be beneficial, and how I might best ramp up if I agree?

    I’m mainly asking because my memory of formal methods is that they were not that useful from the perspective of “I want to build software with the fewest bugs possible” back then, and I very strongly suspect the story is quite different now.

    1. 6

      I’d suggest the author’s entire blog for that. It’s ripe with posts about Alloy and TLA+, in a pretty readable style.

      1. 1

        Hah, thanks! In addition to that, I wrote a thing for my newsletter last week that tries to explain this at a very broad level: A Very Brief Intro to Formal Methods (aka my job).

        1. 1

          That and the links therein were exactly what I was hoping for. Thank you.

    2. 3

      Awesome! I bought the book (Software Abstractions) a few months ago and even if I really enjoyed it (worth every penny in my opinion), an immutable hard copy of a book can’t exactly replace a living, open source online documentation that anyone can improve. Thank you very much!

      1. 3

        I 100% agree that this is a game-changing development for Alloy and for formal methods in general. Could be a huge step forward. Kudos to @hwayne for this undertaking!

      2. 2

        @hwayne,

        How does Alloy fit in with TLA+ in your opinion? Do they compete? Do they solve different problems? If I were to learn just one, which would you recommend?

        EDIT: Another question. Do you see any relation between Alloy and Judea Pearl’s work on causality?

        1. 5

          Crossposting from my HN braindump on this:

          Alloy comes from the Z line of “systems are basically giant relational algebra problems”, while TLA+ comes from the LTL line of “systems are basically giant temporal logic problems”, which leads to a lot of fundamental differences between them. They also had different design philosophies: Jackson wanted a language that was easy to build tooling for, Lamport wanted a language that was easy to express complex logic in.

          One consequence of this is that Alloy is a much smaller language: you can fit the entire syntax on a single sheet. It’s also much easier in TLA+ to write a spec that you can’t model-check, while with Alloy you have to be actively trying. It’s also impossible to write an unbound model in Alloy, so you’re guaranteed that every spec is over a finite state space. Which gets rid of the common TLA+ runtime problem of “is this taking a long time because it’s a big state space or because it’s an infinite state space”.

          Re tooling: Alloy converts to SAT, which makes model checking much, much faster. Specs that would take minutes to check in TLA+ take less than a second in Alloy. Being able to model-find as well as model-check is really nice, as is the ability to generate multiple counter/examples. The visualizer is really useful, too, especially for showing counterexamples to nontech folk. But the thing I honestly miss most when working in TLA+ is the REPL. It’s not the best REPL, but it’s a hell of a lot better than no REPL.

          Okay, so drawbacks: Alloy doesn’t have an inbuilt notion of time. You have to add it in as a sequence sig. This means you can’t study liveness properties or deadlocks or anything like that. It also makes simulating concurrency awkward. This isn’t a huge problem if you have simple interactions or only one structure that’s changing, but the more “timelike” the problem gets, the worse Alloy becomes at handling it.

          Less fundamental but still a big problem I keep having: no good iteration or recursion. Transitive closure is pretty nice but it’s not powerful enough. For example:

          sig node {edge: set Node}
          

          Is N1 connected to N2? Easy, just do N1 in N2^.edge. Through which nodes does N1 connect to N2? That’s much harder.

          The biggest problem with Alloy adoption, though, is social: there’s no comprehensive online documentation. If you want to learn it you have to buy Software Abstractions. Fantastic book but not something that’s especially convenient, and it doesn’t cover newer features. We’re working on changing this, but it will be a while before we have comprehensive online documentation available.

          Which one is more appropriate to use really depends on your problem. As a very, very, VERY rough rule of thumb: TLA+ is best you’re most interested in the dynamics of a system: the algorithms, the concurrency, etc. Alloy is best when you’re most interested in the statics of a system: the requirements, the data relationships, the ontology, etc. My standard demos for showcasing TLA+ are concurrent transfers and trading platforms, while my standard demos for Alloy are access policies and itemized billing. You can use each in the other’s niche, too (see Zave’s work on Chord), so it’s not a stark division.


          If you have to learn just one, it depends on your domain. If you just want to learn an FM for the sake of learning an FM, Alloy’s probably easier to get started in.

          EDIT: Another question. Do you see any relation between Alloy and Judea Pearl’s work on causality?

          I haven’t heard of him! Will check out

          1. 1

            Great answer. Thanks!

        2. 2

          yay!

          now we just need easier concurrency modeling. :)

          1. 1

            FDR might be of interest: https://cocotec.io/fdr/index.html

            (I used to work on it.)

          2. 2

            The title is a bit misleading. It sounds like a documentation generating project (e.g. Mkdocs).

            Here was was scrambling the link thinking: wow alternative to markdown or rst doc generators on the front page!

            1. 1

              Looks good and at the same time, now I really want to buy the book!

              1. 1

                The author notes that this is an unofficial reference. Might I suggest calling it “a reference”, instead of “the reference”?

                There are already existing free references for Alloy. For example, here is an Alloy cheatsheet from the University of Iowa course CS:5810 Formal Methods in Software Engineering.

                There’s a parallel situation in Rust-land: Tokio markets itself as “the asynchronous runtime”. This is confusing, because async-std exists. Anyone can make a runtime. Using the definite article in this way may harm the ecosystem, because it implies that the work is uniquely authoritative, when it arguably is not.

                (The Alloy book “Software Abstractions” is delightful, and I recommend it to anyone with the money to spare. Maybe one day, it will be made available as a free download?)

                1. 13

                  So… the situation right now is weird. It’s officially a first draft of the official reference, and unofficially a reference in its own right. I’m part of the Alloy board and responsible for writing the online documentation. Once I’ve polished the docs a bit more the plan is to host it on the alloytools website. It’s not the official reference, but it eventually will be.

                  For example, here is an Alloy cheatsheet from the University of Iowa course CS:5810 Formal Methods in Software Engineering.

                  I completely forgot to include that cheatsheet in the docs, thanks for reminding me! Though we’re gonna need to update it for Alloy 5…

                  (The Alloy book “Software Abstractions” is delightful, and I recommend it to anyone with the money to spare. Maybe one day, it will be made available as a free download?)

                  Fun fact: I read the entire book in two sittings and then immediately emailed Daniel Jackson raving about how good it is. One thing led to another and now I’m writing docs for him :P

                  Re making it free, my understanding is that the publisher won’t let us. That’s one reason we decided to write an entirely new set of docs.

                  1. 2

                    I’m writing docs for him :P

                    I guess you mean “for everyone” 🙃

                    1. 1

                      Thanks for the clarification!