[sharkbot]

It would seem that the problem is the notion of composition is underspecified in this domain. My intuition would be that one needs a different mechanism of composition aside from the most obvious “use basic logic operators to combine two unrelated logic statements”.

It’s unclear what “the composition of the two systems” really means. Are they running in parallel with no interaction (akin to two AWS instances in different data centers running each program)? Are they running in parallel with superficial interaction (two threads in the same process)? Are they running concurrently with mediated interaction (coroutines)?

The nature of how the programs are composed necessarily would influence the nature of how the specs should be composed, I would think.

Finally, maybe the fault lies with the logic system, rather than the problem?

[hansvm]

I came here to say exactly this. The problem isn't that composing the two specs was hard, but that their desired "composition" required internal details from both specs.

The same difficulty arises in software development too. If the behavior you want isn't just a combination of other existing systems, but rather a combination which peeks inside and hacks on additional constraints then you're going to have a bad time. Maybe it's still worth it for some reason, but that's a leading indicator that a few files probably ought to be refactored.

[mrkeen]

> The problem isn't that composing the two specs was hard, but that their desired "composition" required internal details from both specs.

But there's nothing 'internal'.

In conventional programming we pretend details are internal, e.g. by storing database handles as private fields. But that database is out in the real world.

TLA+ needs to be able to tell you that you can reach a bad state from a particular interleaving of reads and writes to a supposedly internal variable.

[hansvm]

My phrasing could probably have been better there. Do you have any ideas for improvements?

The salient detail is not that you (or at least the verifier) can't reach in and look at the internal bits, but that if your goal is re-use then almost by definition you want to be able to take a whole spec, class, function, ..., and drop it in a new environment without having to wrap it in too many shims and modifications.

Going back to the programming analogy, if the typical way a class was used was by picking and choosing half the private members to reflect over then that would strongly indicate it was a poor abstraction for the current use case. If you wanted to build a system using classes like that as your primitives then you'd incur a lot of development overhead from the impedance mismatch between the thing you want to build and the blocks you're trying to compose to build it with.

TLA+ is a little mathy right? Let's tackle the idea from a different perspective :) The idea behind composability as used by the author is that you want complex specs to be describable as simple functions of simple specs -- C = f(B, A) where f isn't too distasteful. We don't just see that idea in programming and formal models; famous math problems often have that flavor [0], and in general it's pretty common to want to know what you can build from a set of blocks or to design blocks that can build lots of things. The insight the author had is that some things aren't cleanly related in _that_ way even if as humans we can "intuitively" see _some_ kind of a connection.

Drawing a parallel to the real world, if you had two blinker systems (including power and other garbage) each adhering to some kind of blinker spec (always on or off and with some kind of guarantee that you'll keep alternating between those), you'd have a devil of a time composing those two blinkers to create a system of two blinkers which were in sync, whereas with a different set of building blocks it could be easy to create the desired result. The problem you uncovered isn't that the real world is hard to compose though, but that your chosen abstraction didn't fit the problem very well.

[0] https://mathworld.wolfram.com/QuinticEquation.html

[sharkbot]

Just thinking out loud, this feels a bit like the problem ML’s module system is meant to solve: allowing the specialization of modules without needing to uncover the internal details of the implementation. I wonder if some of the same machinery would apply in this case. One would likely need a typed linear temporal logic theory to make it work.