formal verification

The same three theorems from the Python prover, now in Lean 4.

Guillermo Angeris builds a working theorem prover in 61 lines of Julia. A tiny trusted kernel, six axioms, and the compiler does the rest. This article walks through the full construction.

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.

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.

I want to prove Concrete programs in Lean. The compiler already produces native Lean data as its IR, and the language is small enough that formalization might actually be tractable.

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 is a systems language designed so the compiler can reason about what code does: authority, allocation, resource lifetimes, and proof surface.