The Rust Effects Debate and Concrete’s Case for a Smaller Language

9 min read Keywords:  Programming Languages, Formal Verification, rust, Type Systems, lean
A vast imaginary prison interior with towering stone arches, staircases, and walkways receding into shadow
The Gothic Arch, Giovanni Battista Piranesi, 1761

Yoshua Wuyts recently wrote about his “grand vision” for Rust, outlining three directions he thinks the language should pursue: effects, stronger substructural types, and refinement types. The Hacker News thread that followed split predictably: one camp saw a safer, more principled systems language taking shape while the other saw echoes of Scala, C++, and a language that becomes harder to read than the software it is meant to clarify.

Both camps are seeing something real, and I think resolving the tension between them requires something other than adding more features to Rust. That is where Concrete comes in.

#The Diagnosis Is Correct

Forget the specific Rust syntax Wuyts proposes. The strongest part of his post is the problem he identifies.

Rust already has a growing collection of “function colors”: async, const, fallibility, generators, and many other properties that low-level software wants to track. The more of these pile up, the more the language feels like a collection of special cases rather than a single model of what functions can and cannot do.

Systems code needs to express things like:

These matter in practice. Embedded code, kernels, runtimes, critical infrastructure, formal verification, and any codebase where audits are part of the job.

Wuyts is right about all of this. Where I disagree is with the solution. You do not fix this by adding more “colors” to functions inside Rust. You fix it by designing a language where effects are built in from the start.

To make that more concrete, imagine a low-level function that parses input, allocates a buffer, and writes to a file. In Rust, the relevant properties end up spread across different mechanisms: async if it yields, Result if it fails, allocator behavior in the implementation, I/O permissions in convention rather than in the type, and possibly more markers later if the language grows in that direction. In Concrete, the same question is stated in one place: this function is pure unless declared otherwise, and if it allocates and writes a file its signature says with(Alloc, File). The exact syntax does not matter here. What matters is that effect tracking is one model, not a pile of special cases.

The language gets simpler when the effect model is consistent from the start.

#The Complexity Objection Is Also Correct

The skeptics on Hacker News are also right in that languages do not become complex just because they have powerful ideas but because those ideas pile up, and the interactions between them multiply in ways nobody planned for.

Effects interact with async. Async interacts with traits. Traits interact with generics. Generics interact with inference. Inference interacts with macros. Macros interact with diagnostics. Each feature makes sense on its own, but together they can make a language exhausting to read.

The comment that stuck with me was not “I don’t want safety.” It was something closer to: I want to read business logic without feeling that every line is a proof obligation. This objection goes more directly to the tradeoffs of the language, because a language can become “safer” in one technical sense while becoming harder to understand in practice.

I take this concern as a design constraint for Concrete. If a feature makes the language bigger without making ordinary code easier to read, it should not ship. This is why Concrete says no to things that mainstream languages keep around for convenience:

There is a common pattern behind that list: each item either hides work from the reader, creates more than one way to express the same behavior, or forces the compiler and tooling to reason about more implicit interactions. Concrete removes those pressures at the language boundary instead of managing them after the fact. This minimalism is payment towards a bet that stronger guarantees and readability can coexist, but only if the language stays small.

#Effects and Ownership: Yes

Concrete agrees with Wuyts on two of three axes.

Nobody disputes that effects belong in a systems language. The real question is whether you design one model for all of them up front or let them accumulate as special cases. Rust will eventually need a real solution here if it keeps moving in this direction, and this kind of thing is much easier to get right in a new language than in one with a large installed base and a large library ecosystem. What matters is one effect model that handles all of them.

On ownership, Rust is affine: values can be used at most once. That prevents use-after-free in safe code, but it still allows you to forget about values entirely. Concrete goes further. Owned values are linear by default, meaning they must be used exactly once. If you want to prevent resource leaks at compile time instead of hoping for the best at runtime, “at most once” is not enough. In Concrete, the compiler does not silently drop resources for you. Cleanup is explicit with destroy and defer, and if a linear value is not consumed, the program does not compile. This is stricter than Rust, and closer in spirit to Austral. It also costs more. Programmers have to write cleanup paths more explicitly, APIs have less room to paper over ownership decisions, and some common patterns become more ceremonial. I think that is an acceptable price, but it is a real price.

#Refinement Types: No

The main disagreement is refinement types, and this is where I side with the skeptics.

Refinement types are powerful. Pattern types and view types are clever. They can remove runtime checks, express partial knowledge, and make more borrows legal. All true. But they push the language from “the compiler checks resource and effect rules” toward “the compiler expects programmers to encode facts about their programs into types.” That is a very different kind of language from what Concrete is trying to be.

To be precise, I mean Concrete should not put this machinery in the core language. That is different from saying refinement techniques are useless. They may still belong in external proof tooling, verification-oriented libraries, or generated obligations that sit above the language proper. But they do not belong in the center of a language whose main job is to stay small, explicit, and reviewable.

There are three reasons Concrete does not put them in the core language.

First, refinement types dramatically increase what the type checker has to prove. They change the nature of what the compiler is expected to verify, and that change affects the whole language.

Second, it makes code harder to read. Every constraint embedded in a type signature competes for attention with what the code actually does. Programmers can handle refinement types fine. But attention is limited, and type signatures should help you understand a function, not become puzzles on their own.

Third, it works against one of Concrete’s goals: being friendly to machine generation and machine review. Refinement systems are where generated code, human review, and proof tooling start pulling in different directions.

So the breakdown is:

Refinement types are useful in the right context. They are also expensive, and I do not think that cost belongs in the core of a language built around the idea that readability and formal reasoning should help each other instead of competing.

#Smaller, Not Smarter

If you read Wuyts’s post and think “this is Rust becoming more academic,” Concrete might look like it goes even further. It is written in Lean, it talks about kernels and soundness and linearity, and it uses formal language on purpose.

But Concrete is going in the opposite direction: a smaller language with stricter rules. That difference matters. A language becomes hard to read not only when its theory gets deeper, but when there are too many ways to write the same thing, too many implicit behaviors, and too many styles that are all technically valid.

Concrete gets stronger guarantees by taking away options instead of adding them:

If Concrete fails, it will fail for other reasons. Turning into C++ through feature creep is the failure mode the language is built to avoid.

#The Dividing Line

This debate is not really about “type theory versus pragmatism.” It comes down to something more specific: should a systems language get stronger guarantees by becoming more expressive, or by becoming narrower and more explicit?

Rust tries to stay expressive while adding more guarantees. That makes sense for a mainstream language with a large ecosystem. Concrete takes the other path. If a guarantee needs more hidden machinery, more feature interactions, or more inference, I would rather skip it. If a guarantee comes from making the language more explicit, more uniform, and smaller, then I want it.

Systems programming needs better tools for tracking effects and managing resources. The skeptics are right that language complexity is a risk too, and that type-system features become counterproductive when they make the language harder to hold in your head. Concrete accepts the first point and treats the second as a hard constraint.

If Rust is asking how to become safer without becoming unreadable, my view is that this gets much easier when the language is willing to say no to more things. Concrete is not trying to out-express Rust. It is trying to out-constrain it. That is the bet behind Concrete.