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