Three cases of composition and a question

Three examples of compositional type systems are briefly illustrated. The question is whether people working on programming languages and people workingon formal verification feel the need to identify a suite of code reuse/modularization mechanisms for synergically addressing- fine-grained code reuse- coarse-grained code reuse- spatial/temporal code evolution while being suitable for compositional analysis. Perhaps, being suitable for compositional typing could be a preliminary requisite for such a suite of mechanisms. A reformulation of the question: is it feasible for this research community to agree on a list of recommendations / guidelines / principles to be taken into account when designing a new language (or evolving an existing one) in order to facilitate formal verification?