[simiones]

But the article doesn't deal with the possibility/impossibility of verification at all. It deals with the fact that (some?) specifications don't compose elegantly.

That is, that a sufficient specification for System A and a sufficient specification for System B can't be trivially composed into a sufficient specification for a System C = System A + System B. That's not to say that System C can't be specified, but that it can't be specified without re-creating the specifications for System A and System B.

[hwayne]

If I'm being honest, a comment from /u/neel_k on this is enough to make me doubt my entire premise. He's a giant in the field and knows many, many things I don't.