-
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.
-
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
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.