> Are examples out there that show how naive reasoning about languages
> (not individual programs) is a major problem?
> The canonical example is to combine polymorphic let without
> restrictions with naive generalizations for references, exceptions,
> continuations, and channels.
> For what else have we needed *any* form of semantics to dispute naive
Another example of unsoundness resulting from the careless combination
of features that make sense each on its own is the famous
"Inheritance is not subtyping" problem (Cook, Hill, Canning, POPL 89).