Concrete
Mainstream systems languages have grown enormous, but the compiler still mostly says one of two things: it compiles, or it does not. Allocation paths, authority, cleanup, lifetimes, trust boundaries: most of what the program actually does sits just outside what the compiler is allowed to tell you.
Concrete is built the other way around. A smaller surface language. Linear types. Region-scoped borrowing. Explicit capabilities. Visible cleanup. Source contracts and Lean-checked evidence. Each constraint is there to make something visible, so the compiler can answer questions other compilers usually leave to code review.
The series is the case for that bet. Eight essays, each attacking it from a different angle:
- Why Concrete exists. What is missing from the languages we already have, and why making one smaller is the move.
- Rust’s grand vision, Concrete’s answer. What the Rust effects debate gets right, and where a smaller language ends up with cleaner answers.
- The AI training-data trap. Why language ecosystems are getting locked in by the data they leave behind, and how Concrete is designed to escape that.
- Proving Concrete programs in Lean. The original proof-roadmap entry, now updated with what landed: source contracts, proof status, stale detection, and Lean-checked examples.
- When the compiler is the oracle. The most direct demonstration in the series: a compiler that answers semantic questions, not just syntactic ones.
- What Concrete makes worse. The honest list of trade-offs. Smaller languages cost something.
- A fact-producing compiler. Where this is going: compilers that emit machine-readable facts about authority, proof evidence, trust, and runtime risk, not just binaries.
- Nutrition labels for trust. Vitalik Buterin wants software to ship a list of its trust dependencies; this is how a fact-producing compiler already builds the machine-and-math half of that label.
If you want the thesis, start with one. If you want the bet made concrete, jump to five and circle back: the compiler-as-oracle essay is where the whole thing becomes legible at once.
The Problem
Systems languages can enforce safety while still hiding too much of what code actually does. Allocation, authority, cleanup, and trust boundaries often remain scattered across implementation details, conventions, and tooling.
Why Existing Approaches Fail
Mainstream languages usually solve this by adding more machinery or by relying on ecosystem norms. That helps in some dimensions and hurts in others: more hidden behavior, more feature interaction, and less compiler-legible structure.
Our Approach
Concrete takes the opposite path: a smaller language with explicit capabilities, linear ownership, visible cleanup, and a compiler designed to expose semantic facts directly enough for auditing, proof, and automated improvement.
Reference
Living language overview and design reference for Concrete.
Episodes
Episode 1 – Why Concrete Exists
Concrete is a systems language designed so the compiler can reason about what code does: authority, allocation, resource lifetimes, and proof surface.
Episode 2 – The Rust Effects Debate and Concrete’s Case for a Smaller Language
Wuyts is right about effects and ownership. The Hacker News skeptics are right about complexity. Concrete accepts both and says no to refinement types.
Episode 3 – Designing a Programming Language for the AI Era
Edgar Luque is right that AI creates a new barrier for programming languages. He is wrong that the barrier is universal. Languages designed for machine generation and machine verification invert the problem entirely.
Episode 4 – Can I prove Concrete programs in Lean?
The original roadmap for proving Concrete programs in Lean, updated now that part of that bridge exists: source contracts, proof obligations, Lean-checked evidence, stale detection, and an explicit trusted base.
Episode 5 – When the Compiler Is the Oracle
I ran an autoresearch-style loop on a Concrete program. The compiler told an agent where authority, allocation, and proof surface could improve and confirmed when those properties changed. No profiler, no benchmark noise. Your compiler can answer questions instead of saying pass/fail.
Episode 6 – What Concrete Makes Worse
Concrete’s constraints have real costs. Linear cleanup is verbose, hidden-capture closures are gone, and the ecosystem is still early. Here is what the language actually makes harder.
Episode 7 – A Fact-Producing Compiler
Concrete already knows a lot about what a program relies on: authority, allocation, recursion, trust, safety obligations, and proof evidence. The next step is making those facts easy for agents, CI, and reviewers to use.
Episode 8 – Nutrition Labels for Trust
Vitalik Buterin wants trust nutrition labels for software. Concrete shows what the machine-and-math half looks like when the compiler produces it instead of a vendor writing prose.
This series is in progress, stay tuned!