It's very confusing name for this feature. It suggest that some sort of borrowing takes place and that it's just an optional check, which isn't the case. It should be named something like "enforced static usage analysis" instead.
In my programming language I have similar mechanism. But it isn't just checking, since it affects code generation by tracking which variables are still in use and which can be destroyed.
You can very likely borrow check in languages that don't have it in the type system. Exactly the way you suggest, as an optional add-in. It's still WIP but in my side project I haven't found cases that can't be handled yet.
> Exactly the way you suggest, as an optional add-in
No, I don't suggest it, but criticize it. Rust performs its checking as a separate step after actual compilation, which sometimes leads to strange behavior (like borrow errors are shown only after actual compilation errors). I prefer an approach which is integrated with other language mechanisms.
> It's still WIP but in my side project I haven't found cases that can't be handled yet.
It's generally a good idea to write such an analyzer, but I doubt it can be useful without proper integration with the language itself (with huge semantics changes). If it's too strict, it will reject perfectly fine code, but otherwise it will catch only the most obvious errors and approve code having more complex memory bugs.
I think Pony’s reference capabilities are a better solution for linear types. It’s just part of the language so a violation is simply a type error, not something flagged later during static analysis.
In Rust variables are not destroyed after the last borrow ends but instead when it goes out of scope. I guess that is why it us called borrow checking.
> In Rust variables are not destroyed after the last borrow ends but instead when it goes out of scope
That's the problem. Once I had a tricky case, where I locked a mutex in a match expression only to read a single field to match from the mutex contents. In one of branches of the match expression I locked this mutex once again and got a deadlock. Rust compiler wasn't smart enough to realize that the temporary variable for the mutex lock object should be destroyed earlier (it's no longer needed). So, I needed manually reading the field I need into a named variable to eliminate this deadlock.
A more advanced temporaries lifetime analysis would solve problems like described above, but it means basically duplicating a lot of stuff which is already done in the borrow checker (which runs as an afterpass).
A genuine question: is the first point (flow typing / type narrowing) a subset of or intersection with or just an alias to SSA (static single assignment)? I'm playing with a small interpreted language implementation that is based on Lua, and have reached a point where I want to implement a single-pass SSA (there is a nice short CS paper on this), but cannot get my head around all the concepts, even if I need proper SSA for Typescript-like usability.
No. Type systems are unrelated to abstract machines which are unrelated to usability.
Type inference/checking happens early in the pipeline.
SSA is a way of laying out assembly instructions for an abstract machine. I say abstract because real machines re-assign values to the same addresses over time (which is precisely what 'single' static assignment prescribes against). Once you know which registers your real machine has (and instructions), you could take your SSA and turn it into real assembly.
Also, "single-pass SSA"? Not to be too pedantic, but SSA is the destination, not the journey. You could take a single pass to transform from some expressions or statements into SSA, or perhaps from SSA into something else. What's the paper?
At least in my understanding of SSA, its a compiler implementation detail which makes writing optimizations simpler. I imagine you can implement flow typing without SSA.
Completely free flow typing is risky in terms of interpretability, but type narrowing - var a : supertype; if (a is subtype) { // a is known to be subtype }, or type case, saves boilerplate in any OOP language.
I'm not asking about the syntax, I'm asking about the logic where a value can be equal to itself plus another value when the pre-condition is that it must be > 0.
The contract programming in D is pretty much syntactic sugar for placing asserts at different parts of your program.
Refinement types can be used as compile time checks for preconditions and postconditions, while this contract programming is inserting runtime checks.
Here's a good post on the type state pattern in Rust (we don't actually have refinement types in something like Rust but the type state pattern is somewhere closer to refinement types on this spectrum): https://cliffle.com/blog/rust-typestate/
The various contract proposals for Rust are used as input to both formal verification tools as well as input to the optimizer. A good example of one such tool that could utilize contracts is cargo-anneal (https://crates.io/crates/cargo-anneal)
Poor man's runtime "dynamic" version. AKA: A much worse version.
In advanced cases, you'd need dependent types, but the only place where that almost shows up is in the "amount <= balance" assertions. That's also silly because if you typed "amount" and "balance" correctly, then "balance -= amount" has to produce a runtime error because the resulting balance would be negative and not a valid value for the type. So, it's a very natural place anyway to force the programmer to properly handle errors anyways.
"Contracts" has been around a long time and has not caught on. That's usually a good sign that better approaches are prevailing.
In other words: refinement types are a better solution.
contract is way wider than simple refinement types. Refinement types are just a very specific group of invariants.
Contracts are an attempt to include formal specification languages into the implementation languages. You can enforce valid and invalid state changes, enforce relationships across the program state, or even enforce some level of correctness in behaviour.
> around a long time and has not caught on. That's usually a good sign that better approaches are prevailing.
That is completely not true. Plenty of dumb things prevail for faar too long for no other reason than momentum. Plenty of great things remain academic forever. It took decades to get algebraic types or basic functional programming somewhat accepted.
Design by contract is in theory a good idea but suffers from being a pain to use effectively. (making actually useful invariants that help the program more than an assert already would have)
Adding them to languages not built around them also results in quite nasty boilerplate or runtime overhead which further discourage their usage.
I feel like languages are playing around different paints if coat mostly, and not trying to build more meaningful programming experiences.
I'd love to see a language whose pitch is that they have very next level stdlibs builtin. Effect for example is basically a mini stdlibs unto itself. It would be amazing to see such a principled deliberate craft applied to a language. Scope, layers etc etc etc etc: make visible, make first-class the actual pieces of computing, make them part of the language, explicitly modelled.
I'm also super excited for Zena, which just got announced yesterday! A typescript alike that compiles to wasm, and which really leans in to modern wasm, such as gc, wasi. A language that sits well at the cross-roads, that is excellent glue, that runs anywhere, that bridges other languages, is very compelling. https://justinfagnani.com/2026/09/09/zena-a-new-wasm-first-p...
Programming language innovation is measured in decades. I expect LLMs will make it easier to prototype new concepts, but adoption will still progress on a human timescale
The marketing pitch for these things was that they were supposed to induce "cambrian explosion of creations". That there was zero barrier to building anything anymore. This is surely true in programming languages especially, considering how fast LLMs took over software development? Surely this would mean we would get new ideas faster if that was the case? There is literally nothing stopping language designers from getting new concepts out there now even if nobody is using them in production yet.
> LLMs will make it easier to prototype new concepts,
I wonder how soon until we see a language designed for LLMs. I wouldn't be surprised if Anthropic or OpenAI were working on something like that.
No idea what it would look like, but it's pretty likely that "optimized for humans" and "optimized for agents" are not identical. For some class of problem, we really don't need people to be in the code, and I expect that surface area to continue to expand.
Something that is optimized for context efficiency, for example, would be huge. You can go hard on the formalism and correctness, to an extent that would be a pain in the ass for humans but LLMs don't care. Think Rust borrow checker but higher up the stack for a different class of correctness.
I didn't expect this to get posted here. Long time lurker here.
I'm really interested in programming language design and ergonomics. What niche PL features would you like to see have more adoption?
For pedantry, should we note that design by contract came all the way from Eiffel ?
(But it's possible that even less people ever wrote Eiffel than D, so, who knows)
> Borrow Checking
It's very confusing name for this feature. It suggest that some sort of borrowing takes place and that it's just an optional check, which isn't the case. It should be named something like "enforced static usage analysis" instead.
In my programming language I have similar mechanism. But it isn't just checking, since it affects code generation by tracking which variables are still in use and which can be destroyed.
You can very likely borrow check in languages that don't have it in the type system. Exactly the way you suggest, as an optional add-in. It's still WIP but in my side project I haven't found cases that can't be handled yet.
https://github.com/ityonemo/clr
> Exactly the way you suggest, as an optional add-in
No, I don't suggest it, but criticize it. Rust performs its checking as a separate step after actual compilation, which sometimes leads to strange behavior (like borrow errors are shown only after actual compilation errors). I prefer an approach which is integrated with other language mechanisms.
> It's still WIP but in my side project I haven't found cases that can't be handled yet.
It's generally a good idea to write such an analyzer, but I doubt it can be useful without proper integration with the language itself (with huge semantics changes). If it's too strict, it will reject perfectly fine code, but otherwise it will catch only the most obvious errors and approve code having more complex memory bugs.
I think Pony’s reference capabilities are a better solution for linear types. It’s just part of the language so a violation is simply a type error, not something flagged later during static analysis.
In Rust variables are not destroyed after the last borrow ends but instead when it goes out of scope. I guess that is why it us called borrow checking.
> In Rust variables are not destroyed after the last borrow ends but instead when it goes out of scope
That's the problem. Once I had a tricky case, where I locked a mutex in a match expression only to read a single field to match from the mutex contents. In one of branches of the match expression I locked this mutex once again and got a deadlock. Rust compiler wasn't smart enough to realize that the temporary variable for the mutex lock object should be destroyed earlier (it's no longer needed). So, I needed manually reading the field I need into a named variable to eliminate this deadlock.
A more advanced temporaries lifetime analysis would solve problems like described above, but it means basically duplicating a lot of stuff which is already done in the borrow checker (which runs as an afterpass).
A genuine question: is the first point (flow typing / type narrowing) a subset of or intersection with or just an alias to SSA (static single assignment)? I'm playing with a small interpreted language implementation that is based on Lua, and have reached a point where I want to implement a single-pass SSA (there is a nice short CS paper on this), but cannot get my head around all the concepts, even if I need proper SSA for Typescript-like usability.
No. Type systems are unrelated to abstract machines which are unrelated to usability.
Type inference/checking happens early in the pipeline.
SSA is a way of laying out assembly instructions for an abstract machine. I say abstract because real machines re-assign values to the same addresses over time (which is precisely what 'single' static assignment prescribes against). Once you know which registers your real machine has (and instructions), you could take your SSA and turn it into real assembly.
Also, "single-pass SSA"? Not to be too pedantic, but SSA is the destination, not the journey. You could take a single pass to transform from some expressions or statements into SSA, or perhaps from SSA into something else. What's the paper?
Ok. More thoughts.
I was trying to see what was special about Crystal in this regard.
It seems like if you took any ML or Haskell-like, you'd have type inference.
Then you could allow shadowing (Rust-style) meaning the same symbol in the source code would be one variable now, and a different variable later.
Then your compiler would need to distinguish x into x1 and x2 so it could track them separately.
So yeah, kind of an SSA I guess!
At least in my understanding of SSA, its a compiler implementation detail which makes writing optimizations simpler. I imagine you can implement flow typing without SSA.
Can you elaborate what you mean?
What's the nice short paper? (I'd be interested in reading it!)
SSA = static single assignment?
I am confused
Yes, added the expansion
Completely free flow typing is risky in terms of interpretability, but type narrowing - var a : supertype; if (a is subtype) { // a is known to be subtype }, or type case, saves boilerplate in any OOP language.
Looks like its a typo :(
The correct way to go about this would be to return the new balance and capture the return value in the first part of the out postcondition like:
```D double deposit(double amount) in (amount > 0, "Deposit amount must be positive") out (result; result == balance) { balance += amount; return balance; } ```
My mistake!
https://dlang.org/spec/function.html#postconditions
[delayed]
I've never used D, but it appears to be valid syntax. https://dlang.org/spec/function.html#postconditions
I'm not asking about the syntax, I'm asking about the logic where a value can be equal to itself plus another value when the pre-condition is that it must be > 0.
The syntax is correct but I made a logical error since balance is being compared to itself (as opposed to the new balance at the end).
How does contract programming differ from refinement types?
The contract programming in D is pretty much syntactic sugar for placing asserts at different parts of your program.
Refinement types can be used as compile time checks for preconditions and postconditions, while this contract programming is inserting runtime checks.
Here's a good post on the type state pattern in Rust (we don't actually have refinement types in something like Rust but the type state pattern is somewhere closer to refinement types on this spectrum): https://cliffle.com/blog/rust-typestate/
In D, the covariance/contravariance of contract inheritance is an important aspect of the contracts.
The various contract proposals for Rust are used as input to both formal verification tools as well as input to the optimizer. A good example of one such tool that could utilize contracts is cargo-anneal (https://crates.io/crates/cargo-anneal)
Poor man's runtime "dynamic" version. AKA: A much worse version.
In advanced cases, you'd need dependent types, but the only place where that almost shows up is in the "amount <= balance" assertions. That's also silly because if you typed "amount" and "balance" correctly, then "balance -= amount" has to produce a runtime error because the resulting balance would be negative and not a valid value for the type. So, it's a very natural place anyway to force the programmer to properly handle errors anyways.
"Contracts" has been around a long time and has not caught on. That's usually a good sign that better approaches are prevailing.
In other words: refinement types are a better solution.
contract is way wider than simple refinement types. Refinement types are just a very specific group of invariants.
Contracts are an attempt to include formal specification languages into the implementation languages. You can enforce valid and invalid state changes, enforce relationships across the program state, or even enforce some level of correctness in behaviour.
> around a long time and has not caught on. That's usually a good sign that better approaches are prevailing.
That is completely not true. Plenty of dumb things prevail for faar too long for no other reason than momentum. Plenty of great things remain academic forever. It took decades to get algebraic types or basic functional programming somewhat accepted.
Design by contract is in theory a good idea but suffers from being a pain to use effectively. (making actually useful invariants that help the program more than an assert already would have)
Adding them to languages not built around them also results in quite nasty boilerplate or runtime overhead which further discourage their usage.
I feel like languages are playing around different paints if coat mostly, and not trying to build more meaningful programming experiences.
I'd love to see a language whose pitch is that they have very next level stdlibs builtin. Effect for example is basically a mini stdlibs unto itself. It would be amazing to see such a principled deliberate craft applied to a language. Scope, layers etc etc etc etc: make visible, make first-class the actual pieces of computing, make them part of the language, explicitly modelled.
I'm also super excited for Zena, which just got announced yesterday! A typescript alike that compiles to wasm, and which really leans in to modern wasm, such as gc, wasi. A language that sits well at the cross-roads, that is excellent glue, that runs anywhere, that bridges other languages, is very compelling. https://justinfagnani.com/2026/09/09/zena-a-new-wasm-first-p...
Have there been any new good ideas in programming languages since LLMs came around? Or are we over that now..
Programming language innovation is measured in decades. I expect LLMs will make it easier to prototype new concepts, but adoption will still progress on a human timescale
The marketing pitch for these things was that they were supposed to induce "cambrian explosion of creations". That there was zero barrier to building anything anymore. This is surely true in programming languages especially, considering how fast LLMs took over software development? Surely this would mean we would get new ideas faster if that was the case? There is literally nothing stopping language designers from getting new concepts out there now even if nobody is using them in production yet.
> LLMs will make it easier to prototype new concepts,
So where are these prototypes?
Maybe the marketing pitch, like many other pitches, was a lie?
I wonder how soon until we see a language designed for LLMs. I wouldn't be surprised if Anthropic or OpenAI were working on something like that.
No idea what it would look like, but it's pretty likely that "optimized for humans" and "optimized for agents" are not identical. For some class of problem, we really don't need people to be in the code, and I expect that surface area to continue to expand.
Something that is optimized for context efficiency, for example, would be huge. You can go hard on the formalism and correctness, to an extent that would be a pain in the ass for humans but LLMs don't care. Think Rust borrow checker but higher up the stack for a different class of correctness.