The semantics of OO languages is really messy and complicated and probably has the least well understood theory of all sequential forms of computing.
Much of this has to do with the root: most of our PL theory was basically designed for FP, and applying them to OOP has been predictably difficult. Most PL theoreticians are more interested in FP than OOP, so progress is quite slow (though see work done by Ross Tate, Igarashi, etc...for progress).
soundness question when considering variance
As an example, let's assume that you have two classes, Cat and Dog, both inheriting from Animal, and that you have a covariant mutable List implementation.
Say you have a value of type List[Cat]. Since List is covariant, this value can legally be passed to a function that expects a parameter of type List[Animal].
Now, imagine you have a function that expects a List[Animal] and adds a Dog to it. That's a legal operation: Dog extends Animal and can thus be used this way.
Putting the two together, you have a perfectly legal way of adding a Dog to a List[Cat], which a sound type system should not allow. An example of that is Java's Array, which is both covariant and mutable, and that as a result can yield type errors at runtime.
But I thought that was pretty well understood, so I don't know what he thinks is open...