-
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.
-
Theorem Proving
Writing Your First Proofs in Lean
The same three theorems from the Python prover, now in Lean 4.
-
Theorem Proving
Programming a Mini-Lean in Julia’s Type System
Guillermo Angeris builds a working theorem prover in 61 lines of Julia. A tiny trusted kernel, six axioms, and the compiler does the rest. Here is the construction.
-
Theorem Proving
Building a Tiny Theorem Prover in Python
A tiny theorem prover is just a term language, a checker, and a small trusted kernel. We build one in plain Python to make the architecture explicit.
-
Theorem Proving
Propositions Are Types, Proofs Are Programs
The Curry-Howard correspondence says that types and logical propositions are the same thing. Understanding why changes how you think about both programming and mathematics.
-
Concrete
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.
-
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
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.