Thanks, this seems like a perfectly coherent definition of compositional. I think my earlier confusion was a purely terminological matter.

Regarding "What you're saying is that proofs can be composed. That is true, but unhelpful, as it doesn't make proofs easy." I agree that the ability to compose proofs does not make proof easy. But I would push back somewhat against the idea that this is unhelpful.

The ability to prove, in isolation, the relevant properties about some entity (e.g., a function, a hardware module, or what have you), and then to make use of these properties, without ever looking inside the entity again, to prove properties of some larger system, seems to me to be absolutely essential for scaling proofs to large systems.

This ability is of course completely common in tools like interactive proof assistants, but is less common in more automated procedures.