Concrete
Concrete is a series about a systems language designed so the compiler can say more than pass or fail.
If you are new to the series, start with Why Concrete Exists. If you want the most practical demonstration first, read When the Compiler Is the Oracle. If you want the living reference material, use Concrete Spec.
Suggested reading order:
- Why Concrete Exists
- The Rust Effects Debate and Concrete’s Case for a Smaller Language
- The AI Training Data Trap for Programming Languages Has an Exit
- Can I prove Concrete programs in Lean?
- When the Compiler Is the Oracle
- What Concrete Makes Worse
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 – The AI Training Data Trap for Programming Languages Has an Exit
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?
I want to prove Concrete programs in Lean. The compiler already produces native Lean data as its IR, and the language is small enough that formalization might actually be tractable.
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, no closures hurt composition, and the ecosystem barely exists. Here is what the language actually makes harder.
This series is in progress, stay tuned!