As we're seeing more and more language features originating from functional programming trickle into mainstream languages, this research hasn't clearly gone to waste even though everyone is not programming in functional programming languages.
imperative programming is not very interesting from a programming language theory point of view.
All that has changed in the last decade or so, but it will take another decade or so before recent research insights into non-functional languages perlocates down to accessible textbooks.
We hope that this cost can be lowered in the future.
The industry tends to lag behind academia by at least a couple decades. In the 90's, lots of research was being devoted to functional programming and the various applications of type systems. Now we see various companies starting to use languages like Haskell and ocaml. Nowadays, it seems like dependent types and program verification are popular in academia, so maybe we'll see some of that by 2030.
First of all, you need to correctly define the specification. Saying "the returned list is sorted" isn't enough because that would also accept lists that have nothing to do with the input, like [1,2,3,4,5]. Also saying that the list only contains elements from the input is also not enough because that would accept a returned list with duplicated or missing elements. To really make a specification that models what you want you need to say that the returned list is a sorted permutation of the input list.
Then, once you manage to get a formal specification that is actually what you want prout invariantving it is also hard. In the bubble sort case you need to figure you need to write down the proofs in detail, down to the point when you use the fact that comparison is a transitive relation.
I don't know, I find GCL and predicate transformer semantics to be quite interesting. Esterel's approach to synchronous reactive systems, too.
I don't see why the research potential in imperative languages couldn't be ripe. The semantic possibilities are large. A ton of PL and OS research from ETH Zurich, Xerox PARC and Bell Labs alike have been from imperative language designs.
If you find that condescending and/or narrow-minded, you're not alone. There are more things in programming language theory than are dreamt of in their philosophy (to steal a line from Shakespeare).
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...