| HN Mirror

Hillel, you called me out on Twitter so I felt like it would be best if I elaborated for a few reasons. Firstly, hopefully it will be reassuring to know that although my comment seemed glib I was actually trying to engage with the substance of your work, secondly, it will help clarify my thoughts, and thirdly, someone else may be interested.

I don't have any experience with machine-verified specifications but I do have experience writing computer programs and (traditional, human-checked) mathematical proofs, so my comment comes from that perspective.

Regarding

> Me: 200 words on how we're talking about composing specifications, not code, because specifications aren't programming languages

> HN: [parent]

I'm sorry if the use of the terminology "programming language" was jarring. I tend to take the point of view that a huge range of human activity in what are traditionally called programming languages, probabilistic graphical models, languages for constraint solving and optimisation, a lot of mathematics (especially category-heavy mathematics) and even writing YAML for configuration is actually all just different aspects of the same thing. I chose the word "programming" in the parent which might betray some bias on my part but regardless of the word chosen the practice of combining smaller logical pieces into larger logical pieces is common to all. Your article is suggesting that there is something about the nature of specifications that makes this composition harder than it is for executable code.

The conclusion may be true (I have no idea) but I'm afraid that I just don't see how your article justifies it. In the first example I see a language LTL whose design encourages users to write small logical units that cannot be composed[1] easily with the && operation. A more awkward encoding does achieve compositionality (through stuttering-invariance). It looks like TLA+ provides notation to make it more natural to write the small logical units in ways that they can be composed easily with &&. That makes it sound to me like TLA+ is a better language than LTL (for this purpose)! Better languages make it easier and more natural to write smaller units in ways that can be composed. That's all my parent comment says!

In the second example it is composition with && itself that proves to be impossible. The composition rule is something more complicated:

    Next = (NextX(z) && Same(y)) || (NextY(z) && Same(x))
    Spec = InitX && InitY && □[Next]_xyz

Unless I'm missing something, there's nothing wrong or hard about that composition rule, it's just the tooling that doesn't make it easy to work with. In Haskell we compose monadic functions with >>=. That would make life really awkward unless we had do notation. The problem is not that monadic functions are hard to compose, it's that the language needs to support them ergonomically. I can't see anything in your post that suggests to me that specifications are by nature hard to compose. All I can see is unergonomic languages.

[1] composed in the sense which your article elaborates, that is, in a way which combines the properties of both in some desirable way