Type Systems
Not the keyword you're looking for? See all keywords.
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. This article walks through the full construction.
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.
Fede’s Guide to Type Systems: From Generics to Dependent Types
A practical guide through the landscape of type systems, from everyday generics to dependent types that prove correctness, with examples in Rust, Scala, and Idris
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.