concrete

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.

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.

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.

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.

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.

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.

Concrete is a systems language designed so the compiler can reason about what code does: authority, allocation, resource lifetimes, and proof surface.