I (briefly) used Eiffel in the 1990s. It had some of, if not the, worst tooling I've ever experienced for a programming language, and I've used COBOL compilers and MVS. A pretty nice language, but the software tool support initially was appalling.
That was due largely to the designers of the language, Bertrand Meyer and his wife, creating the tools. The tools, the seminars, and the books were primary income streams.
Interesting, I wasn't aware of that, although it certainly felt like academic-grade code, which someone once described to me as "thrown together by a caffeine-crazed grad student at 3am and run on at least one test case". It's a real pity because there were some really good ideas in there, but the required tooling would have been just too much for just two people to assemble out of whole cloth.
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.
In rust it's a lot closer to optional: you can in principle compile rust without doing any borrow checking at all (and I believe in practice mrustc does not bother to implement it, because it's primarily used for bootstrapping and so assumes it is already being passed code that compiles with regular rustc).
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).
Rust already supports the kind of behaviour you are describing for borrows, because of non-lexical lifetimes. Code like the following now compiles:
fn main() {
let mut x = 42;
let y = &x;
println!("{y}");
let z = &mut x;
}
Even though y's scope overlaps with z's, and they introduce conflicting borrows, this code compiles because the compiler treats y's borrow as dead after its last use (this has been true since Rust Edition 2018, so for quite some time now). If you move the println after the mutable borrow then it fails to compile.
However values whose types have Drop are another matter. They are treated as if there's an explicit call to their drop function at the end of their lexical scope which pins their lifetime. This is intentional and desirable precisely because of the guard pattern (like for mutexes).
If you didn't have that guarantee, at worst your mutex's guard object would be immediately dropped because it's never referenced after it's created, or at best it would be very tricky to understand what the protected critical region is.
> If you didn't have that guarantee, at worst your mutex's guard object would be immediately dropped
For named local variables it's a different story. They should remain alive until the end of their lexical scope. But for unnamed temporaries created in expressions different rules should apply - as soon as there is no reference to such temporary, it should be destroyed.
Typically, a temporary's lifetime is bounded by the statement it is in, but for the subject of a match, this extension overlaps with all its arms even if the temporary borrow is not used after the subject is evaluated (i.e. you borrowed, you read and copied a field out of the borrow).
The issue seems to be that this is a syntactic transformation, but the expected behaviour requires type information, so you can tell whether to extend the temporary's lifetime by whether that lifetime leaks the immediately containing scope.
This is kind of similar to how type parameter unification in Hindley-Milner works. There's even an analogy made between the two things here:
I know it's controversial but I really do love C++26's contract assertions.
I find they enable you, your consumers, IDEs, agents, etc understand the contracts of a method far faster, as it means you don't actually have to read the full method body. If the pre condition is correct and the post condition fails then you can be fairly sure the bug report goes to whoever owns that method, as either the precondition is wrong or the method is wrong.
I’m a big fan of checked exceptions, which are niche in the sense that only Java has them (at least among popular programming languages). However, Java lacks the ability to parameterize code over sets of exception types, which places limitations on how checked exceptions can be used with type-generic code. That’s something that can be improved.
Exceptions allow more flexibility in separating the success-case program flow from the error-case program flow, compared to return codes or union return types. Unchecked exceptions, however, have the same drawbacks as dynamic typing does. Checked exceptions are the static-typing equivalent.
Row types are great. I'm doing a PureScript project right now and absolutely love having row polymorphism.
I'm also a fan of effect systems, although I haven't used them as much. Having an IO type in Haskell is great, but the ergonomics aren't (among other things, you get async-like function coloring). Effects seem like a much nicer, more composible way to get the same benefits.
Generic narrowing types / linear types (like if you check that a string has length 10, then its type knows, and functions accepting bounded strings can accept it.)
This makes it easier to split raw inputs from validated inputs and delimiting where they are used in the code.
If you're serious about doing OO with static typing as well as (of course) mutability, you basically have to have something like flow typing to keep away the circle/ellipse nonsense. (In so far as flow typing is really static typing at all!)
So while the ideas discussed are interesting, the origins are a bit off.
Flow typing, is actually called Flow-sensitive typing.
Contracts were introduced into the industry via Eiffel, which continues to be sold via Eiffel Software company.
By the way, at the recent DConf 2026, during the panel discussion, contracts was actually one of the features that were discussed as something that they would remove from the language, if doing it all over again.
Rust's borrow checker, is based on Affine Types, and the first systems language that looked into it was Cyclone, which AT&T started as research project in colaboration with an university, to eventually replace C.
I can see how it can be useful to start with a broad type, e.g. a union, and narrow it down in a block. However, I don't quite get the opposite direction shown in their example (first an int, then a string, then a union).
Same rationale as flow valuing. Some people like values being reassigned, and some people like types being reassigned.
You might be reading too much into the union example. The checker just doesn't know if the middle block ran, so maybe it remained an int, or maybe it became a string.
Nice list. I have a new language I'm working on (called Zena: https://zena-lang.dev/) with all of these in some form:
If you have static types and unions, control-flow analysis and narrowing is critical for avoiding an excessive amount of casts - and if you also have pattern matching, you get very nice style where a type-check, state extraction, and branch are all one expression.
Borrow checking. Zena is a GC'ed language, but it runs in Wasm and lots of Wasm resources are external, so Zena has affine types and second-class values for managing resources and disposing of them when no longer used. GC + borrowing is a great combo because you don't need borrowing for everything and lexical lifetimes with a few escape hatches cover most things. The ownership system is also great for modeling structured concurrency.
I'm working on contracts after borrow checking is complete. My impetus there is AI-generated code. If humans still review at all, reviewing the contacts more than the implementations makes managing large amounts of changes easier.
I'd like to see a few more good ideas spread:
Formal verification. Contracts should be a good stepping stone into a spec language, from there a proof language and checker. This should also be good for AI-generated code.
Numeric unit types / units of measure with dimensional analysis. We should be able to say that a variable isn't just a f64, but a f64 of meters, and when divided by seconds, give a velocity. I don't know why this hasn't made it into more mainstream languages, but it seems like it makes programs more clear, not just statically safer. For synax, my plan is to parameterize scalars by units, like f64<m> vs f64<s> and have units like `m` and `s` be associated with dimensions like `length` and `duration`.
Async cancellation. I added cancellation as a first-class language concept in Zena so that it can be handled like exceptions, but aren't exceptions. It extends try/catch to try/catch/cancel/finally. When a task is canceled, a cancellation unwinds the stack starting from the next suspension point (await). The benefit here is that you don't have to remember to check for cancellation in async functions - they're all cancellable.
Zena looks super cool! I was wondering if you could walk me through this syntax thats part of the example loops:
```
let iterator = items.[Iterable.iterator](); // <--- this part in particular is confusing me
while (let (true, item) = iterator.next()) {
console.log(`next: ${item}`);
}
```
Dimensional types and formal verification make me super excited to see more of this language.
You also probably mention this somewhere and I'm missing it, but any thoughts on adding pure functions / more general mutability enforcements?
This is similar to JS, where you can access properties of an object dynamically with [] notation, but Zena is static and doesn't have any reflection (yet) so the symbol has to be declared and statically resolvable, and Zena has operator overloading an a [] operator so we need a way to differentiate between symbol-keyed access from indexed access ([]), thus the o.[] syntax.
I do want to add pure functions, especially for compile time constants. I want to add a macro system that can either run pure functions (on the AST or IR, not sure yet) at compile time, or run arbitrary code sandboxed in a Wasm module.
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?
My idea was that with single pass, I can build SSA form during AST construction, and use phi-nodes to update type flow info. Then I could use SSA form to prove that I can use certain optimized bytecode instructions when a variable/register is known to be of certain type (I have virtual registers and fat instructions, eg ADD takes 2 sources and destination). Maybe I'm mixing control flow, type flow and SSA. I do not understand where I should stop with the pipeline if I use bytecode/VM.
The paper is: Brandis, Marc M., and Hanspeter Mössenböck. "Single-pass generation of static single-assignment form for structured languages." (https://bernsteinbear.com/assets/img/brandis-single-pass.pdf). It was quite understandable to me. For a deeper dive with proper SSA construction with dominance frontiers I could not find time to dig deeper, many other papers on SSA require focused CS work on them, not practically feasible for a side project. Also, single-pass is a requirement for very fast compilation to bytecode and LSP feedback.
I tried to read TS and Pyright source code, they share the same style of immense files and nested local functions, that was quite a steep wall to understand actual inner workings in detail. Maybe TS implementation in Go will be easier to read, it's on my later TODO list. It's tempting to use AI for help, but I'm quite experienced already with undoing AI work when it takes a wrong direction and I do not notice early.
Yep, this sounds like conflating two different ideas about SSA.
You could parse a source language with shadowed variables into an AST, and then one of your earliest AST transforms could be a 'de-shadowing' pass. The resulting AST would only see variables assigned only once.
Then a type-inference pass, where your AST expressions would gain type info.
(Then a bunch more passes, e.g. closure conversion if you have them)
Then towards the end you could lower your typed AST into a typed instruction list (having the SSA property - but nothing to do with allowing variables and their types to shadow earlier in the pipeline)
Shadowing at AST level with the lexical scope is easy to implement, it's just each usage looks up inside out to parent scopes. But if we treat each assignment as a kind of shadowing, it works in a similar way and turns into a kind of SSA. The complexity arises with phi-nodes when multiple paths join. I think the confusion comes from the strict definition of SSA as something useful for the very late stage in the pipeline, but the same concept can exist much earlier in the pipeline.
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.
HN does not use markdown code block formatting so this is hard to read. Formatting code blocks is simple, two blank spaces before any line to make it a code block and no need for extra newlines (unlike between paragraphs):
double deposit(double amount)
in (amount > 0, "Deposit amount must be positive")
out (result; result == balance)
{
balance += amount;
return balance;
}
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.
This "flow typing" looks very intriguing to me: So, in s sense, what we know as "dynamic typing" is more precisely describable as "runtime" (not compile-type) dynamic typing?
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 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.
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.
> Poor man's runtime "dynamic" version. AKA: A much worse version.
Contracts don't have to be evaluated dynamically, that's just one way they're implemented. See SPARK/Ada for an example of contracts being used to prove programs statically, not just test them dynamically.
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...
Most of my research conversations with Claude nowadays are basically about this—what it would take to make every latent bit of program semantics visible and expressible in the language itself. As you put it, first-class everything.
At this point I think we have good solutions for expressing pretty much all the most common program semantics, but there’s no language that brings them all together under a unified syntax, tooling, etc.
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,
We don’t need new ideas, we need languages that take the best ideas developed over the past decade of PL research and operationalize them in a language with modern tooling and build support.
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)
Racket also added contracts around the same time that D did.
I (briefly) used Eiffel in the 1990s. It had some of, if not the, worst tooling I've ever experienced for a programming language, and I've used COBOL compilers and MVS. A pretty nice language, but the software tool support initially was appalling.
That was due largely to the designers of the language, Bertrand Meyer and his wife, creating the tools. The tools, the seminars, and the books were primary income streams.
Interesting, I wasn't aware of that, although it certainly felt like academic-grade code, which someone once described to me as "thrown together by a caffeine-crazed grad student at 3am and run on at least one test case". It's a real pity because there were some really good ideas in there, but the required tooling would have been just too much for just two people to assemble out of whole cloth.
> 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.
> It suggest that some sort of borrowing takes place
It does. A value is passed by reference, borrowing it from the owner.
> and that it's just an optional check
I don't see how the word "check" implies that it's optional.
In rust it's a lot closer to optional: you can in principle compile rust without doing any borrow checking at all (and I believe in practice mrustc does not bother to implement it, because it's primarily used for bootstrapping and so assumes it is already being passed code that compiles with regular rustc).
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.
> but I doubt it can be useful without proper integration with the language itself
So projects like mypy or sorbet aren't useful because they aren't properly integrated?
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).
Rust already supports the kind of behaviour you are describing for borrows, because of non-lexical lifetimes. Code like the following now compiles:
Even though y's scope overlaps with z's, and they introduce conflicting borrows, this code compiles because the compiler treats y's borrow as dead after its last use (this has been true since Rust Edition 2018, so for quite some time now). If you move the println after the mutable borrow then it fails to compile.However values whose types have Drop are another matter. They are treated as if there's an explicit call to their drop function at the end of their lexical scope which pins their lifetime. This is intentional and desirable precisely because of the guard pattern (like for mutexes).
If you didn't have that guarantee, at worst your mutex's guard object would be immediately dropped because it's never referenced after it's created, or at best it would be very tricky to understand what the protected critical region is.
> If you didn't have that guarantee, at worst your mutex's guard object would be immediately dropped
For named local variables it's a different story. They should remain alive until the end of their lexical scope. But for unnamed temporaries created in expressions different rules should apply - as soon as there is no reference to such temporary, it should be destroyed.
Okay, I see. The issue you are running into is specifically mentioned in this article about how Rust currently does lifetime extension:
https://smallcultfollowing.com/babysteps/blog/2023/03/15/tem...
Typically, a temporary's lifetime is bounded by the statement it is in, but for the subject of a match, this extension overlaps with all its arms even if the temporary borrow is not used after the subject is evaluated (i.e. you borrowed, you read and copied a field out of the borrow).
The issue seems to be that this is a syntactic transformation, but the expected behaviour requires type information, so you can tell whether to extend the temporary's lifetime by whether that lifetime leaks the immediately containing scope.
This is kind of similar to how type parameter unification in Hindley-Milner works. There's even an analogy made between the two things here:
https://okmij.org/ftp/ML/generalization.html#gen-mismanageme...
I know it's controversial but I really do love C++26's contract assertions.
I find they enable you, your consumers, IDEs, agents, etc understand the contracts of a method far faster, as it means you don't actually have to read the full method body. If the pre condition is correct and the post condition fails then you can be fairly sure the bug report goes to whoever owns that method, as either the precondition is wrong or the method is wrong.
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?
I’m a big fan of checked exceptions, which are niche in the sense that only Java has them (at least among popular programming languages). However, Java lacks the ability to parameterize code over sets of exception types, which places limitations on how checked exceptions can be used with type-generic code. That’s something that can be improved.
Exceptions allow more flexibility in separating the success-case program flow from the error-case program flow, compared to return codes or union return types. Unchecked exceptions, however, have the same drawbacks as dynamic typing does. Checked exceptions are the static-typing equivalent.
Row types are great. I'm doing a PureScript project right now and absolutely love having row polymorphism.
I'm also a fan of effect systems, although I haven't used them as much. Having an IO type in Haskell is great, but the ergonomics aren't (among other things, you get async-like function coloring). Effects seem like a much nicer, more composible way to get the same benefits.
Generic narrowing types / linear types (like if you check that a string has length 10, then its type knows, and functions accepting bounded strings can accept it.)
This makes it easier to split raw inputs from validated inputs and delimiting where they are used in the code.
If you're serious about doing OO with static typing as well as (of course) mutability, you basically have to have something like flow typing to keep away the circle/ellipse nonsense. (In so far as flow typing is really static typing at all!)
Yes... But I think this only tells half of the story.
What if you pass a reference and mutate the object inside the function?
So while the ideas discussed are interesting, the origins are a bit off.
Flow typing, is actually called Flow-sensitive typing.
Contracts were introduced into the industry via Eiffel, which continues to be sold via Eiffel Software company.
By the way, at the recent DConf 2026, during the panel discussion, contracts was actually one of the features that were discussed as something that they would remove from the language, if doing it all over again.
Rust's borrow checker, is based on Affine Types, and the first systems language that looked into it was Cyclone, which AT&T started as research project in colaboration with an university, to eventually replace C.
Could someone explain the appeal of flow typing?
I can see how it can be useful to start with a broad type, e.g. a union, and narrow it down in a block. However, I don't quite get the opposite direction shown in their example (first an int, then a string, then a union).
Same rationale as flow valuing. Some people like values being reassigned, and some people like types being reassigned.
You might be reading too much into the union example. The checker just doesn't know if the middle block ran, so maybe it remained an int, or maybe it became a string.
Nice list. I have a new language I'm working on (called Zena: https://zena-lang.dev/) with all of these in some form:
If you have static types and unions, control-flow analysis and narrowing is critical for avoiding an excessive amount of casts - and if you also have pattern matching, you get very nice style where a type-check, state extraction, and branch are all one expression.
Borrow checking. Zena is a GC'ed language, but it runs in Wasm and lots of Wasm resources are external, so Zena has affine types and second-class values for managing resources and disposing of them when no longer used. GC + borrowing is a great combo because you don't need borrowing for everything and lexical lifetimes with a few escape hatches cover most things. The ownership system is also great for modeling structured concurrency.
I'm working on contracts after borrow checking is complete. My impetus there is AI-generated code. If humans still review at all, reviewing the contacts more than the implementations makes managing large amounts of changes easier.
I'd like to see a few more good ideas spread:
Formal verification. Contracts should be a good stepping stone into a spec language, from there a proof language and checker. This should also be good for AI-generated code.
Numeric unit types / units of measure with dimensional analysis. We should be able to say that a variable isn't just a f64, but a f64 of meters, and when divided by seconds, give a velocity. I don't know why this hasn't made it into more mainstream languages, but it seems like it makes programs more clear, not just statically safer. For synax, my plan is to parameterize scalars by units, like f64<m> vs f64<s> and have units like `m` and `s` be associated with dimensions like `length` and `duration`.
Async cancellation. I added cancellation as a first-class language concept in Zena so that it can be handled like exceptions, but aren't exceptions. It extends try/catch to try/catch/cancel/finally. When a task is canceled, a cancellation unwinds the stack starting from the next suspension point (await). The benefit here is that you don't have to remember to check for cancellation in async functions - they're all cancellable.
Zena looks super cool! I was wondering if you could walk me through this syntax thats part of the example loops:
``` let iterator = items.[Iterable.iterator](); // <--- this part in particular is confusing me while (let (true, item) = iterator.next()) { console.log(`next: ${item}`); } ```
Dimensional types and formal verification make me super excited to see more of this language. You also probably mention this somewhere and I'm missing it, but any thoughts on adding pure functions / more general mutability enforcements?
Thanks!
So `items.[Iterable.iterator]()` is invoking a symbol-keyed method.
It's declared like:
This is similar to JS, where you can access properties of an object dynamically with [] notation, but Zena is static and doesn't have any reflection (yet) so the symbol has to be declared and statically resolvable, and Zena has operator overloading an a [] operator so we need a way to differentiate between symbol-keyed access from indexed access ([]), thus the o.[] syntax.I do want to add pure functions, especially for compile time constants. I want to add a macro system that can either run pure functions (on the AST or IR, not sure yet) at compile time, or run arbitrary code sandboxed in a Wasm module.
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?
My idea was that with single pass, I can build SSA form during AST construction, and use phi-nodes to update type flow info. Then I could use SSA form to prove that I can use certain optimized bytecode instructions when a variable/register is known to be of certain type (I have virtual registers and fat instructions, eg ADD takes 2 sources and destination). Maybe I'm mixing control flow, type flow and SSA. I do not understand where I should stop with the pipeline if I use bytecode/VM.
The paper is: Brandis, Marc M., and Hanspeter Mössenböck. "Single-pass generation of static single-assignment form for structured languages." (https://bernsteinbear.com/assets/img/brandis-single-pass.pdf). It was quite understandable to me. For a deeper dive with proper SSA construction with dominance frontiers I could not find time to dig deeper, many other papers on SSA require focused CS work on them, not practically feasible for a side project. Also, single-pass is a requirement for very fast compilation to bytecode and LSP feedback.
I tried to read TS and Pyright source code, they share the same style of immense files and nested local functions, that was quite a steep wall to understand actual inner workings in detail. Maybe TS implementation in Go will be easier to read, it's on my later TODO list. It's tempting to use AI for help, but I'm quite experienced already with undoing AI work when it takes a wrong direction and I do not notice early.
Yep, this sounds like conflating two different ideas about SSA.
You could parse a source language with shadowed variables into an AST, and then one of your earliest AST transforms could be a 'de-shadowing' pass. The resulting AST would only see variables assigned only once.
Then a type-inference pass, where your AST expressions would gain type info.
(Then a bunch more passes, e.g. closure conversion if you have them)
Then towards the end you could lower your typed AST into a typed instruction list (having the SSA property - but nothing to do with allowing variables and their types to shadow earlier in the pipeline)
Shadowing at AST level with the lexical scope is easy to implement, it's just each usage looks up inside out to parent scopes. But if we treat each assignment as a kind of shadowing, it works in a similar way and turns into a kind of SSA. The complexity arises with phi-nodes when multiple paths join. I think the confusion comes from the strict definition of SSA as something useful for the very late stage in the pipeline, but the same concept can exist much earlier in the pipeline.
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!
Yes, a lexical scope with shadowing
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!)
Brandis, Marc M., and Hanspeter Mössenböck. "Single-pass generation of static single-assignment form for structured languages." (https://bernsteinbear.com/assets/img/brandis-single-pass.pdf).
SSA = static single assignment?
I am confused
Yes, added the expansion
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
HN does not use markdown code block formatting so this is hard to read. Formatting code blocks is simple, two blank spaces before any line to make it a code block and no need for extra newlines (unlike between paragraphs):
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).
This "flow typing" looks very intriguing to me: So, in s sense, what we know as "dynamic typing" is more precisely describable as "runtime" (not compile-type) dynamic typing?
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.
Borrow checking (as frustrating as it is) is a good idea. I never knew about invariants in D, and now I want them in my language 's classes!
But flow typing? That seems like a footgun...
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.
> but it's pretty likely that "optimized for humans" and "optimized for agents" are not identical.
Why?
> we really don't need people to be in the code
Code exists for humans, if only for safety reasons.
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.
> Poor man's runtime "dynamic" version. AKA: A much worse version.
Contracts don't have to be evaluated dynamically, that's just one way they're implemented. See SPARK/Ada for an example of contracts being used to prove programs statically, not just test them dynamically.
My rcc C compiler has a compile-time contracts and range/interval prover also. Needs -O3.
For full formal proofs it's easier to use cbmc or esbmc though
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...
Most of my research conversations with Claude nowadays are basically about this—what it would take to make every latent bit of program semantics visible and expressible in the language itself. As you put it, first-class everything.
At this point I think we have good solutions for expressing pretty much all the most common program semantics, but there’s no language that brings them all together under a unified syntax, tooling, etc.
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?
> That there was zero barrier to building anything anymore. ... Surely this would mean we would get new ideas faster if that was the case?
No, of course not. The point is that the tools comprehend the idea and implement it. Not that they have the idea for you.
We don’t need new ideas, we need languages that take the best ideas developed over the past decade of PL research and operationalize them in a language with modern tooling and build support.
https://www.reddit.com/r/AIprogrammingLanguage/
Maybe the marketing pitch, like many other pitches, was a lie?
> So where are these prototypes?
I'm working on one, but you're not going to like it.
If LLMs are writing code, won't adoption progress on LLM-timescales? Humans would seem to be out of the equation.