1. 11
  1. 6

    CICS is one of the most successful pieces of software in the world: there are over 30 000 licences, and most of the world’s top companies use it.

    Ooof. Looks like the book is from 1996, so it’s a bit of an extravagant claim even at the time.

    Fun fact: Daniel Jackson got so fed up with Z that he invented Alloy just to fix the shortcomings!

    1. 4

      CICS was the primary reason I worked on porting Swift to z/OS. COBOL interaction was the holy grail. (I left before we got to that point and I don’t know the status of things since then.) Point being that CICS plays a large role in finding the IBM compiler efforts.

      It should also be noted that the book was written on OS/2, so maybe they were getting those numbers from the IBM sales team. ;)

      1. 1

        Swift-COBOL interaction reminds me of the time I got multiprotocol routing set up between IP, IPX, AppleTalk, and SNA.

        it worked, somehow.

      2. 2

        It’s most successful, for suitably small values of “most”.

        1. 2

          The small most hypothesis.

      3. 3

        The cool thing about this book is that it’s a big pile of techniques you might apply with or without Z. I’ve found that one can also use a subset of them without mathematical proof just to add a bit more rigor to software development. That’s often called “semi-formal” verification. An example is looking at input/output ranges for data, their ordering, and quick calculations on how the control flow might affect them to estimate correctness.

        1. 2

          Tangential question, but do you think that formal methods will get more traction in the 2020s? Aside from building more robust software, I think semantics can help AI approaches such as program synthesis.

          I did a whole MSc on the topic back a decade ago, and we were using a mix of old references like the one posted and new more polished material. I remember quite fondly using these books, on a language inspired by Z: http://www.imm.dtu.dk/~aeha/RAISEbooks.html

          The literature is much better now. In particular there is some great broad introductory material:

          Plus some classics, most available long ago already:

          And some constructive foundations:

          1. 3

            I have been summoned

            Almost exactly a year ago I wrote a piece called Why Don’t People Use Formal Methods which aimed to cover a lot of the specific difficulties in the space. To summarize:

            1. Proving code is correct is pull-your-hair-out hard
            2. Proving designs correct is easier, but has social barriers.

            Now (1) is getting easier, as the SMT revolution comes into full force, but it’s probably going to be a specialist domain for the near future. I’ve talked with people who do it professionally, and the challenges there are all essential. Proving code correct is just a fundamentally difficult problem. We’re likely to see more advances in partial verification, though, with things like Rust showcasing what we can push into the language.

            Re (2), the biggest challenges there are accidental: formal specification has bad UX and bad PR. I’ve been working really hard on the second one, making things like TLA+ and Alloy easier to learn by providing better education materials and more interesting to learn by providing lots of good examples. But the UX problem is still a pretty big barrier. Fortunately, it’s something that can change, and probably will as more and more people start to learn these things.

            1. 1

              I totally agree SMT solvers, when blended into languages, will make things more usable.

              I really liked Spec# as a student a decade ago. I think their approach of applying theorem proving on contracts yields a very natural user interface. I suspect that when applied on a language with very clean semantics, such as any purely functional one, it’d be even better.

              Do you have any other favorite tools aside from TLA+ or Alloy? What is the domain you are mostly working on?