← All repos

concrete

Concrete is a simple programming language specifically crafted for creating highly scalable systems that are reliable, efficient, and easy to maintain.

GitHublambdaclass.github.io/concrete/
mlirprogramming-language
Browse cluster: Cluster 50 →
2,310commits
14contributors
11languages

Tech stack & purpose

Concrete is a programming language designed for creating highly scalable, reliable, and maintainable systems. The language is built around an evidence-based framework where every construct is classified into one of five evidence states—proved, enforced, reported, assumed, or trusted—with proof states further refined into kernel-decision, partial, or stale substates. The project uses MLIR (Multi-Level Intermediate Representation) as part of its implementation and includes extensive examples and documentation demonstrating runtime-safety obligations such as array bounds checking, division-by-zero prevention, and integer overflow detection. The compiler prioritizes kernel-checked reasoning (constant folding, omega solver, and Lean's bv_decide tactic) before reaching for external SMT solvers, reserving external solvers only for genuinely nonlinear problems that kernel tools cannot handle. The repository also contains research notes on language design, standard library shape, compiler architecture, proof workflows, and tooling—suggesting active ongoing development with no single named author or institution identified in the materials provided.

Community & reference links

Languages

Lean
44.8%
Shell
28.1%
Rust
23.2%
Typst
1.6%
Python
0.9%
Makefile
0.6%
C
0.3%
HTML
0.2%
TeX
0.1%
CSS
0.1%
Nix
0.0%

Contributors