Somewhat unrelated to this link, but I really think that it’s interesting how much effort we put into the theory side of languages/types - with almost no one in industry applying these lessons. The essence of this is just something along the lines of “What if we unified values with types, so we could have more useful type checking?” We have billions of dollars being spent and thousands of smart people working for decades, who don’t even get to use a proper type system - forget about statically-checked polymorphism or dependent typing. It’s not even as if we lost the ball, we’re running in the wrong direction. It’s almost trivial to bolt on gradual typing to a language. It’s also not too hard to retrofit dependent types (just don’t bother with Turing-incompleteness). The whole point of these type systems is to better model systems, so why not go the extensible route of letting anyone hook into the “type checking” phase? Import affine types (that decades old thing that got rust popular); write your own domain-specific checker, even. It’s so frustrating to see how beautiful ideas just die because we feel comfortable the way things are now. Maybe language was the wrong abstraction to begin with. Sorry to derail, but this feels like the only path to truly popularize the lambda cube as a concept.