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.
People will get mad at me for saying this but... this isn't that deep. As with most things in academic CS, this is just a formalization of stuff that is very common practical engineering.
> 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
The name of the paper is "data types as lattices" so data not programs as such and denotational semantics is about programs. So I'll say:
1. A language independent representation of a data type is just a protobuf (or whatever your favorite serialization/deserialization framework is);
2. The language of lattices is very common in eg compilers (eg grep for lattice in LLVM) but again it's cart before the horse kind of stuff because there's not much there to be exploited in representing your unions and intersections as meet and join;
3. A language independent representation of operations is an IR and indeed you can inductively derive certain facts about some language level features (across multiple languages) by analyzing the IR. Again cf LLVM
I realize the paper is from 1976 so someone will pop up and say "the paper inspired these things" but it's just not true; people generally follow their nose when implementing and then someone comes along and says "let's name it a lattice".
This isn't a hot-take or something, it's just experience from being on both sides of the fence.
ozb|1 year ago
almostgotcaught|1 year ago
> 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
The name of the paper is "data types as lattices" so data not programs as such and denotational semantics is about programs. So I'll say:
1. A language independent representation of a data type is just a protobuf (or whatever your favorite serialization/deserialization framework is);
2. The language of lattices is very common in eg compilers (eg grep for lattice in LLVM) but again it's cart before the horse kind of stuff because there's not much there to be exploited in representing your unions and intersections as meet and join;
3. A language independent representation of operations is an IR and indeed you can inductively derive certain facts about some language level features (across multiple languages) by analyzing the IR. Again cf LLVM
I realize the paper is from 1976 so someone will pop up and say "the paper inspired these things" but it's just not true; people generally follow their nose when implementing and then someone comes along and says "let's name it a lattice".
This isn't a hot-take or something, it's just experience from being on both sides of the fence.
arunaugustine|1 year ago
[1]: https://cuelang.org/docs/concept/the-logic-of-cue/#the-value...