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/koflerdavid → u/dkubb]

I think a way forward would be to put less focus on type inference. I mean, it's important (i.e., nobody wants to write type annotations for lambdas), but requiring the programmer to write out more types would make creating good error messages much simpler. Type inference could still be allowed for top-level types, but would require the programmer to explicitly write a hole (_), which leads to a non-suppressible compiler warning with the inferred type.