I read this paper some 10 years ago, and have always wondered whether these ideas are implemented in industry. I know people use Denotational Semantics in academia, but eg I want an actual language that can encode the language-independent "meaning" of both a c++ template library and a Python program in a composable way, and also express and prove refinement relations between different specifications and implementations.