I can program a contract that can be parameterized with an address of some other sub-contract (then, say, store it in variable), which I call to do some particular logic. If I change that sub-contract address, I can effectively change my contracts logic. Is that what you?

I would like to mention an interesting paper regarding the topic: Marino, Juels - Setting Standards for Altering and Undoing Smart Contracts (2016).

I see your point about 'pure notions of correctness'. While I agree that some interesting properties of a contract is not easy to come up with (and hence verify), I still believe that there are some 'safety' properties which are far easier to articulate.

I also believe that there is an element of modeling: it may be a viable way of validating properties.