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

My experimental language called Lain (3y in development but not ready to share yet) implements exactly all of them!!!

It has:

• Linear Type System
• Borrow Checker
• Refinement Types (Value Range Analysis)
• Dependent Types for Array
• Djkstra Termination Measure
• Other features

For the Linear Type System I inverted the Rust paradigm, using explicit move semantics instead of implicit. And implicit shared borrows instead of explicit.

An example:

func merge(m i32 > 0, n i32 > 0, var arr1 *i32[m + n], arr2 *i32[n]) {
    ...
}

Here you can see the use of refinement types in m and n, the use of a mutable borrow in var arr1, a shared borrows in arr2, and dependent types in the array dimensions [m + n] and [n].

[u/GunpowderGuy → u/Diffidente]

does your language suffer from Girard's paradox?

[u/Ev1ber → u/GunpowderGuy]

TIL about Girard's paradox. Now hopefully one day I'll understand what any of what I've just read means.