1. 38
  1.  

  2. 6

    This comes right on time, I’m attempting to introduce formal models to my team at $WORK, and have been going through so many materials (lots of them by you) these past few days. Will check this out today! Thank you!

    1. 5

      PLEASE let us know how it goes. I’ve got a couple of failures under my belt when it comes to such efforts. Would love to compare notes and learn.

      1. 3

        I have yet to have it take on at work at all. Even lighter weight things like property-based testing are outside of the comfort zone of a lot of people. I will say, what has piqued the most curiosity is when you show someone relevant to something they’re working on, instead of speaking philosophically / abstractly.

        For example, today I was able to draw up a quick proof in Isabelle to show that introducing a feature flag to a code path wouldn’t break the existing behavior when the flag was disabled. Simple example, but it was received well.

        1. 3

          Now that I think about it, property-based testing sounds like a much easier sell than “formal methods” proper. It’s really just a variation on unit testing, which is official industry “best practice” now (for good or ill). For programmers who already write lots of asserts, the notion of invariants should already be familiar. And once you have your team sold on property-based testing, formalizing invariants in a spec should be a little easier (I hope).

          1. 2

            Absolutely - properties and theorems are expressed the same way, theorems just must be proven. With property-based testing, you’re just evaluating the property with tons of input data and saying “even though we haven’t proven this, we’ve never observed it to be false.” That’s empiricism at its finest, and it’s something people are more open to than math proofs.

            This also offers a way to start with property-based testing and “upgrade” to proof if you choose to. They’ve written about this on the Cogent team, where they’re using exactly that workflow for formally verified file system implementations. No use trying to prove something that doesn’t even pass a property-based test.

            The way I sell property-based testing is that it’s also generally way less actual work to write the test. If you have to write test data generators, they’re written one time and reused between different properties. Test setup can be soul crushing, so it’s a way to automate the boring stuff away. That’s in line with the “practical programmer” ethos.

        2. 1

          I keep trying to introduce this on a team wide scale at the $WORK but so far its really just crazy ol kstatz12 tinkering in his imagination closet

          1. 1

            I can’t even get my colleagues to read my informal correctness proofs, so not sure how I’d sell them on formal methods…

            1. 1

              tell them that folks practicing formal methods at a $dayjob today, will be the ‘data scientists with exuberant pay options’ of tomorrow.

              My thinking is that the ‘break through’ will be called ‘compile-time testing and verification’, and it will happen when major languages and their toolchains (including compile time debugging) will integrate formal methods into them.

              There will be ‘learn formal methods in 21 days’ books and boot-camps, a million of youtube videos about how to ‘Ace an interview for compile-time testing and verification jobs’, recently graduated students coming your place of work and asking when you are going to get off a dinosaur-way of doing things.

              There will be companies going public that will list, ‘formally verified’ software as their ‘competitive advantage’. Manufacturing, robotics will be touting that their formally verified software powers the world… … And so on.

              … And, perhaps, the data science be remembered as a historically-relevant attempt to derive business value from log files :-)

        3. 4

          Given this new feature (and accepting some quirks before it’s fully baked in), is there a useful short primer for an ignoramus like me on what sort of problems Alloy is suited for vs TLA+, assuming I wanted to throw a week at learning one or the other over the xmas vac?

          1. 4

            Regarding style and tone: this is incredibly well-written and the examples are simple enough to be tractable but rich enough to stay illustrative. I felt like I could follow the article appropriately even if some of the finer points remain above my head. Hopefully diving in and doing some sketching will help that. Well done, @hwayne.

            Regarding the substance and content: I am very excited to dig into Alloy 6 and very curious how the new book by the Alloy team will shape up. In particular, I wonder how they will position Alloy relative to other tools in the space where TLA+, is only one example.

            I’ve used Alloy in the past and feel strongly that my time with it was productive, particularly when I formally specified an algebra I’ve been working on for some time to get the structures right. These new temporal aspects will only improve my ability to specify it by adding a whole new dimension. Curious what other users think.

            1. 5

              I’m one of the Alloy 6 authors. As far as I know, there are not so many mature formal tools that can nicely be used to specify both structural and causal aspects of a system (that is, mixing first-order and temporal reasoning). So I’d say TLA+ (which we also use, mainly in teaching but also for some research work) remains the principal object of comparison. If you want to model an algorithm that you can express easily in PlusCAL (e.g. an algorithm with many sequential parts and interruptions at various points) or if you want to carry out full proofs (there is an Isabelle backend for this), then TLA+ is a tool of choice.

              It is therefore not very relevant for Alloy to address the exact same problems as TLA+. Our main focus has rather been to try to improve Alloy’s own strengths, in particular the fact it’s really good to model and analyze requirements or high-level designs, and to find flaws quickly and automatically. Indeed (1) the language is quite flexible (thanks to the ability to state -no pun intended- global, temporal properties about your system); (2) the variety of temporal connectives (incl. past ones) can be handy for some properties (e.g. “in any state, a node in a ring is elected as a leader if and only iff it has received its own address”: always all n: Node | n in Elected iff once (n.address in n.mailbox)); (3) model finding is performed up to a user-specified bound and the tool leverages the fact that some objects are constant or mutable to improve efficiency; and (4) finally the Visualizer is really nice, in particular with its new trace exploration capabilities.

              1. 4

                I’m one of the Alloy 6 authors.

                First, thanks for responding. Second, thank you SO much for all your hard work. Your many efforts have been noticed and noted by many appreciative folks. Congrats on the release and occasion!

                It is therefore not very relevant for Alloy to address the exact same problems as TLA+.

                Your explanation from the previous paragraph makes this conclusion follow very closely and I think I get your point about this bit:

                Our main focus has rather been to try to improve Alloy’s own strengths, in particular the fact it’s really good to model and analyze requirements or high-level designs, and to find flaws quickly and automatically.

                I have had some difficulty introducing Alloy at me workplace but the following is growing. Luckily my selling points are consistent with the high-level design practices associated with iterative specification. I have a funky name for it so it sounds acceptable to corporate ears but “Test-Drive Architecture” and associated terminology isn’t particularly descriptive.

                Again, thanks a ton for your efforts and reply. Feel free to reach out if you’re interested in further dialog. Wishing you and the team the best!

                Thanks, +Jonathan

                1. 2

                  It is therefore not very relevant for Alloy to address the exact same problems as TLA+.

                  Your explanation from the previous paragraph makes this conclusion follow very closely and I think I get your point about this bit:

                  I probably wasn’t very clear here. What I meant is that there’s added value in expanding what Alloy is already particularly good at (namely scenario exploration and quick bug-finding in designs, all in a user-friendly language and tool). While if you have the kind of problems for which TLA+ already shines, you should most certainly use TLA+.

                  (Thanks for the appreciation.)

                  1. 1

                    Thanks for the followup!

              2. 2

                I felt like I could follow the article appropriately even if some of the finer points remain above my head.

                Can I ask which finer points went over your head? It’s good feedback for me.

                1. 2

                  Yes, but I can also say that your aside on how TL is hard made me feel better. Right at home, even.

                  I think most of the time the finer points of Alloy itself go over my head when I can’t remember just what exactly the transitive closure of a relation does! Is that sufficient or would quotations help more?

              3. 3

                It’s hard to describe how much of a game changer this is for Alloy. Before this, dealing with time was painful. It was just dreadful. I only used Alloy to model static data models because of this. Now, it’s wrapped up in a nice bow with very Alloy-like sharp terminology and semantics.

                Great decision from the Alloy maintainers to include these features - this issue might have caused Alloy to fade into obscurity.

                And, thank god for @hwayne. Something about his POV and message resonates much more with “working” programmers it seems like. I think this will end up doing a lot of good for humanity in the long run. Yea, formal methods are always going to be based in theory, but there are plenty of ways to apply them at work. And you can’t have as much fun with them by yourself, so we need more adopters on the job.

                1. 3

                  The future⁺ is now.

                  1. 2

                    Rather than future⁺ and future⁻, try future and <future, as in “present ≤ future”. (They are supposed to be superscripted, but lobsters is not being compliant.)