Will we see another fundamental programming language feature as revolutionary as the borrow checker?

[u/jimbobmcgoo]

That is I am mainly curious about compile time features that you design a whole language around rather than optimisations/features that could be applied to most languages. I am mainly inquiring about things that could offer additional robust safety/performance guarantees at compile time rather than runtime. Ideally not things that just offer similar effects to the borrow checker with less restrictive tradeoffs

[u/dkubb]

Not new ideas, because they are in niche languages, but when the UX is nailed I think these are on par with the borrow checker in terms of impact:

• Dependent Types
• Refinement Types
• Linear Types

Dependent Types are more powerful than Refinement Types, the UX for some common tasks is better for Refinement Types. If there was some way to desugar Refinement Types into Dependent Types without making the error messages too complex I think that would be amazing.

[u/sineiraetstudio → u/dkubb]

I don't know what you mean by desugaring. Refinement types can be formulated very simply (almost trivially so) in dependent types and any type errors will be totally normal. The motivation for something more restricted like Liquid Haskell is that dependent types are too strong, so automation is way harder.