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