1. 28

  2. 4

    Note this covers the same content as Everything About Distributed Systems is Terrible. This is a more “canonical” link, though, plus the following differences:

    • Proper title (“everything is terrible” was a joke title)
    • Includes some commonly-asked questions, and answers
    • Copy of the formal spec used as an example

    Not sure what the Lobsters protocol is in this case. Delete this post? Merge this into the other post? Merge the other into this?

    1. 3

      I merged the other post in to this one. The time between submissions is long for a merge, don’t make a habit out of it. Your reasoning for it is sound, however.

      1. 1

        I say don’t worry about it since only one is on the front page. I’m glad you mentioned it since I didn’t know other one was yours from the title. I saved it to look at later. Now, I’ll just watch this one instead since it has more info.

      2. 3

        Thanks, @hwayne, that was a really interesting video, and right at the level for me (has read something about TLA+, can remember the order those letters come in in the acronym).

        How do you go from a spec to code in production?

        Carefully. Verifying that code matches a spec, aka refinement, is a really hard problem! To accurately implement your spec, you need good engineers, good tooling, and good process. Nothing can take those needs away.

        This seems like an opportunity: not to automate the thinking, but to automate getting to the point where the thinking can be applied. Are there tools that can go “up” the abstraction stack from code (the most refined version of the spec) to more abstract forms?

        I think it’d be useful both in itself, and as a way to help adopt this way of thinking, if there were a way to compare the designed spec to a derived spec, even if just at the “not glaringly different” level. It seems like it might be something a symbolic executor could produce from the code?

        1. 2

          The keywords you’re looking for are “extracting,” “learning,” “generating,” and so on… “formal specifications,” “models,” and “properties”… “from code.”

          Those will net you all kinds of projects like that which will then tell you what terms to search for from there. Relevant to this thread are these slides on extracting TLA+ from C code. Another that detects invariants in programs is Daikon. I don’t have a lot of examples off top of head, though, since almost all work starts at the specifications, analyses for properties, and then generates code from specifications. The stuff analyzing code is usually a black box with its own internal format (eg static analyzers, model checkers).

        2. 2

          I think this talk is the gateway drug because I ended up carving for more and bought the book, help?

          hwayne, you speak like a teacher. Very pleasant to listen to.

          1. 1

            Good talk! For people wanting to learn more, there is a video series on the TLA+ homepage. https://lamport.azurewebsites.net/tla/tla.html