-
Essay
A Proof Is Only as Good as Its Spec
Formal verification doesn't eliminate risk. It relocates it into the spec, the model, and the trusted base. Five runnable Lean 4 proofs that compile cleanly and still sit on real bugs.
-
Essay
Fede’s Guide to Type Systems: From Generics to Dependent Types
A practical guide to type systems, from everyday generics to dependent types that prove correctness, with examples in Rust, Scala, and Idris
-
Concrete
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.
-
Concrete
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.
-
Concrete
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.
-
Concrete
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.
-
Concrete
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.
-
Concrete
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.
-
Concrete
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.