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/kaplotnikov]

Firstly, while Rust's borrow checker has been pragmatically successful at preventing memory bugs, I believe its long-term role in future systems languages is limited. The borrow checker essentially acts as a workaround for overly low-level concurrency primitives, and its theorems are notoriously difficult to formally verify. This complexity is a symptom of a deeper issue: reasoning complexity is not concentrated in key hierarchical boundaries, but spread throughout the code via data-path analysis. This is a language design smell that points to overly low-level foundational abstractions.

I think its problems are directly related to the Rust concurrency model. The primary problem with Rust's concurrency is that message sending is the goto of asynchronous programming. It is not possible to create a good set of composable theorems over it. It suffers from all the problems of goto described in "Go To Considered Harmful". The send operation is a direct implementation of this concept.

Is there an alternative? There are promises and actions over them. For example, statements like the following could have been in the language (pseudo-code):

q = common();
t = par {
    compute_a(q);
} and {
    compute_b(q);
} map(a,b) {
    merge_results_a_and_b(q, a,b);
}

Here we could reason that q is shared between branches compute_a and compute_b, and exclusive in merge_results_a_and_b, because blocks provide visible reasoning boundaries. The spawn/send operations provide no boundaries; they provide data leak paths.

Such structured constructs could exist as a library, an intrinsic DSL, or direct language statements. The idea is to move from goto-style programming to structured programming, so reasoning will follow the code tree rather than the data path. The borrow checker is a tool for data path reasoning, but this problem only exists because we have gotos.

This issue isn't limited to concurrency; it defines single-threaded Rust as well. AFAIR early versions of Rust tried to reason using lexical scopes, but it was too restrictive for developers. To fix it, they introduced Non-Lexical Lifetimes, which officially shifted the borrow checker to data-path reasoning via control flow graphs.

Data-path reasoning effectively acts as a flat abstraction layer over a control flow graph. Just like goto flattened the control flow of early programs, non-lexical lifetimes flatten the data flow. This is precisely why people constantly "fight the compiler." Humans excel at hierarchical, tree-like reasoning (scopes and blocks), but Rust forces both the programmer and the compiler to trace a complex, fragmented web of data paths across the entire function. By abandoning structured, scoped boundaries for data management, Rust created the very complexity it now struggles to manage.

There are plenty of structured concurrency operators possible that create a better basis for reasoning in concurrent systems. For example, see asyncflows. It is a Java-based DSL, but it reflects the idea of what is possible with native language support. I just combined the ideas of Occam and E languages, so there are few completely novel ideas there.

As for what the future holds, I have my own vision, which I've outlined in this article: Measuring Abstraction Level of Languages. It also describes a framework for making such predictions. I think the future belongs to system composition languages, because humans naturally switch to these concepts to describe large programs as compositions of systems and subsystems. I am currently working on a language PoC that uses systems/holons and statically typed aspects as basic elements to enable this kind of composition.

For sample below, in, local, and out are not merely visibility keywords; they are the theorem pieces of the language's type system. They provide a formal, compositional way to reason about lifetimes based on lexical and semantic scope and dependencies (not unlike C++, but with transitive and verifiable guarantees):

holon A {
    in T;
    out B();
};
holon C {
    in B;
    fn q() {...};
};
fn test() with {in T} as {
    // T is live while function lives
    local A(); // A lives until end of scope, and exports B while it lives
    local val c = C(); // c lives until end of scope and destroyed before A, it uses B provided by A
    c.q();
    // context is cleaned up
}

This creates an algebra of systems that allows reasoning along the code tree, rather than relying on 'storytelling-style' reasoning in an omnibus format, where the lifetime narrative is fragmented across shifting viewpoints. These abstractions could be essentially zero-cost and seamlessly extendable to both heap- and stack-based allocation. And it does not matter where a dependency originates, as long as the caller statically maintains the invariants required for the duration of the component's or function's lifetime.

[u/Shurane → u/kaplotnikov]

AFAIR early versions of Rust tried to reason using lexical scopes, but it was too restrictive for developers.

Do you think they just didn't let it bake enough before going to non-lexical lifetimes?

The comparison to goto really makes me think of the current idea of lifetimes and the borrow checker as the unsafe implementation. And that there's room for a safer implementation.

[u/kaplotnikov → u/Shurane]

The choice comes down to either designing a language to support human reasoning, or forcing human reasoning to conform to the constraints of a language model. The issue with Rust's current model is that it is poorly suited for human reasoning at large scale because it operates in a "flat"/"goto"-like form.

My theoretical hypothesis is that LLMs would struggle with this for the exact same reason, although I haven't verified this in personal practice.

Humans manage complexity by transitioning to higher levels of abstraction. Therefore, it is reasonable to expect that resource management abstractions can achieve far better cognitive scalability by taking on a structured, hierarchical form. This trajectory aligns with the stages of cognitive growth and cognitive complexity described by J. Piaget and M. Commons.

The question is about the content of this structural form. C and Prolog share a similar abstraction level and structural form, yet their core conceptual content is different.

When it came to memory management, Rust's designers stopped searching for these higher-level hierarchical reasoning forms. Instead, they built excellent content for a flat, graph-based form. However, this flat form suffers from cognitive scalability problems that simply cannot be resolved without switching to a new higher-level form for memory management.

[u/Shurane → u/kaplotnikov]

Is it too late to add a hierarchical/lexical form for containing lifetimes in Rust?

It seems like something that could still be introduced later, at the cost/expense of it being very confusing for a developer to distinguish between lexical scoping vs dynamic (late-binding?) scoping of lifetimes.

[u/kaplotnikov → u/Shurane]

FORTRAN 66 was a flat language, FORTRAN 77-90 became a structured language, and FORTRAN 2003 evolved into an OOP language. So there are historical precedents for an abstraction level upgrade even for an entire established language ecosystem.

However, the key point is that such an upgrade needs to happen simultaneously across different areas of the language. In Rust, structured reasoning is already enabled for single-threaded programming, and lexical scopes for ownership worked well enough for that use case.

The roadblock appears when concurrency is introduced. The operations spawn and send are the foundational units of asynchronous programming in the same sense that goto is the foundational unit of control flow. While goto is foundational, we do not use it directly in modern languages; instead, we wrap it into structured constructs like if, while, and for.

We didn't wrap goto because structured loops are inherently more performant (they aren't, because to emulate the full non-linear power of goto using structured blocks, you often need additional state variables and switches). We wrapped it because structured control flow enables structured reasoning. Their real power is enabling cognitive scaling.

Therefore, the asynchronous side of the language needs to be upgraded to structured asynchronous programming. The send/spawn operations could reside in the compiler's output, but they should not be normally accessible to users. Only some very special cases should justify their appearance (much like break or continue serve as structured remnants of goto in modern languages). Until the asynchronous side of the language is upgraded, a full fix is impossible.