Why Concrete Exists

7 min read Keywords:  Programming Languages, Formal Verification, Type Systems, lean, concrete
Abstract composition of black lines forming rectangles filled with primary colors on a white background
Tableau I, Piet Mondrian, 1921

This is the foundation piece for the Concrete series. If you want the most practical demonstration first, start with When the Compiler Is the Oracle. If you want the living language reference, use Concrete Spec.

Systems programming has a recurring problem. We want to write code close to the machine, but we also want to make strong claims about what that code does. Does it allocate? Does it touch the network? Does it leak resources? Can it be audited without tracing twenty helper functions and three layers of library convention?

Most languages answer those questions indirectly. You read the implementation. You profile. You infer from style. You trust unsafe blocks, docs, and review discipline. Even in strong languages, much of what matters about a program lives outside the type system.

Concrete exists because I think that is the wrong place to stop.

Concrete is a systems language built around a single organizing principle: every important property the compiler can know about a program should be explicit enough for humans and machines to act on directly.

#The problem

The usual systems-language tradeoff is framed as performance versus safety. That is real, but it is not the only tension that matters.

There is another one:

When a language gets more implicit, more inferential, and more feature-rich, the gap between “what the code does” and “what the compiler can state plainly” gets wider. Destructors run invisibly. Allocation hides inside convenience patterns. Effectful behavior is ambient. Trust boundaries collapse into one broad unsafe bucket. Code remains writable, but it gets harder to audit, harder to prove, and harder to optimize from semantic facts rather than benchmark noise.

Concrete is an attempt to push in the other direction: a narrower language that gives up convenience so the compiler can expose more truth.

#The core bets

Concrete makes five bets.

1. Effects belong in function signatures. If a function reads a file, allocates, touches the clock, or calls the network, that should be visible in its type via capabilities such as with(File) or with(Alloc). No ambient authority, no guessing from implementation detail.

2. Ownership should be linear by default. Rust’s affine ownership prevents use-after-free, but it still lets you forget a value and let Drop clean up behind your back. Concrete is stricter. Owned values must be consumed exactly once. Cleanup is explicit with destroy and defer. That is more ceremonial, but it means resource lifetimes are part of the visible program rather than a hidden compiler action.

3. Hidden behavior is the enemy. No implicit destructors, no hidden allocation, no operator overloading, no closures with invisible captures, no exceptions unwinding through code you cannot see. When you read a function, the goal is that you are looking at what actually executes.

4. Smaller beats cleverer. I do not want a language that keeps absorbing more machinery in exchange for stronger guarantees. I want one effect model, one ownership model, one small grammar, and a core language that still fits in a human head.

5. The compiler should produce structured knowledge, not just pass/fail. If the language is explicit enough, the compiler can report things like capability usage, trust boundaries, allocation sites, public interface surface, and proof-eligible subsets. That changes how humans review code and how automated agents improve it.

#What that looks like in practice

This design leads to a specific kind of language.

A pure function is pure because it declares no capabilities and the compiler proves that claim through the call graph.

A function that allocates says with(Alloc).

A function that can read files says with(File).

A function that crosses a foreign or semantically dangerous boundary says with(Unsafe).

A function that manages a resource shows its cleanup in the source with defer destroy(x).

A piece of low-level implementation trickery can be marked trusted, separating internal pointer-level unsafety from externally visible semantic authority.

The result is not just “safer C” or “stricter Rust.” It is a language whose semantics are meant to be legible enough that the compiler can answer higher-level questions directly.

That is why the later posts in this series focus on things like:

#What Concrete is for

Concrete is not trying to be the best language for everything.

It is aimed at code where hidden behavior is expensive:

These are domains where “what can this function do?” is not a stylistic question. It is an audit question. Sometimes it is a certification question.

For those domains, I think a smaller and more explicit language is a better trade than a more ergonomic and more magical one.

#What Concrete is not for

Concrete is not a convenience-first language.

It is worse than Rust or Zig at many pleasant things:

That is not accidental. It is the price of the design. A later tradeoffs post will make that cost explicit in more detail.

I think those costs are worth paying for some domains and not worth paying for others. The point is not that Concrete has no downsides. The point is that the upsides and downsides come from the same constraints.

#Why Lean matters

Concrete’s compiler is written in Lean 4. That started as a practical implementation decision, but it has architectural consequences.

Every Concrete program becomes native Lean data as it moves through the compiler pipeline. That creates a path, still incomplete but very real, from systems code to proof tooling without stitching together two unrelated ecosystems. It also encourages a language shape that can actually be formalized: small core semantics, explicit effects, explicit ownership, limited implicit machinery.

I do not think “written in Lean” is the main reason to care about Concrete. The main reason is the language design itself. But Lean makes the long-term verification story more plausible than it would be otherwise.

#What exists today

Concrete is no longer just a sketch. The compiler is a real Lean 4 codebase with a staged pipeline, a substantial test suite, an expanding standard library, and audit-oriented report modes.

What does not yet exist is just as important:

So the right way to read this series is not “finished language announcement.” It is “a case for a particular design direction, with some parts already working and others still being built.”

#Where to go next

If you want the rest of the argument, read the series in roughly this order:

  1. Why Concrete Exists
  2. The Rust Effects Debate and Concrete’s Case for a Smaller Language
  3. The AI Training Data Trap for Programming Languages Has an Exit
  4. Can I prove Concrete programs in Lean?
  5. When the Compiler Is the Oracle
  6. What Concrete Makes Worse
  7. A Fact-Producing Compiler

If you want the language details rather than the essay version, use Concrete Spec.

That is the bet behind Concrete: not a more expressive systems language, but a more legible one. A language that constrains the programmer so the compiler can say more that is actually useful.