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.
See also https://www.haskellforall.com/2016/04/worst-practices-should...
[1] composed in the sense which your article elaborates, that is,
in a way which combines the properties of both in some desirable
way