Concrete

Concrete is a systems programming language designed for safe and predictable code, with semantics defined by a small core calculus formalized and proven sound in Lean. It combines linear types, static capability tracking, and region-scoped borrowing to provide compile-time guarantees about resource usage and side effects.

Episodes

Episode 1 – The Concrete Programming Language: Systems Programming for Formal Reasoning

This series is in progress, stay tuned!