The Concrete programming language
Concrete is a verification-oriented systems language for code whose authority, allocation, failure modes, ownership, and evidence should be visible in source and reports.
It is linear rather than affine: non-Copy values must be consumed explicitly. Capabilities such as File, Console, Alloc, and Unsafe appear in function types. Proofs, runtime checks, oracle tests, assumptions, and trusted boundaries are reported as separate evidence classes.
The refusals are the point: no closures, no trait objects, no macros, and whole-program monomorphization keep callable values inside a closed set of named functions. A function-pointer target may still be chosen at runtime, but its possible targets are statically enumerable. That gives facts about authority, allocation, and failure a tractable path from main to whole-program claims.
fn read_u16_be(packet: [u8; 512], off: i32, len: i32) -> i32 {
if off < 0 || off + 2 > len { return -1; }
let hi: i32 = packet[off] as i32;
let lo: i32 = packet[off + 1] as i32;
return hi * 256 + lo;
}
fn report(result: i32) with(Console) {
if result < 0 { println("out of range"); }
else { println("ok"); }
}Compiles as-is with concrete main.con; the report below is its real output.
Getting started
Concrete is experimental. The most honest first contact is to build it, run the gates, and inspect the reports. You need Lean 4, lake, and clang; the make targets wrap the build in the repository's Nix flake. See the installation guide for the plain lake build path.
$ make build
$ make test
$ .lake/build/bin/concrete examples/base64_cli/src/main.con --report audit
$ .lake/build/bin/concrete examples/png_chunks/src/main.con --emit-trace-jsonMain ideas
Linear ownership
Copy is explicit. Other values are moved, returned, consumed, or destroyed by a visible operation such as defer x.drop(); the compiler does not insert hidden scope-end destructors.
Capabilities
Hosted effects are authority, not folklore. A function that reads files, writes to a console, allocates, crosses FFI, or uses unsafe code has to say so in its type and reports.
Second-class references
References flow downward into calls and callbacks. They are not returned from functions. This avoids lifetime syntax and keeps ownership facts small enough to audit.
Evidence accounting
Concrete does not collapse evidence into one green badge. Lean proofs, kernel decisions, SMT checks, oracle tests, runtime checks, assumptions, and trusted code are different facts.
A report is part of the program
Reports are meant to answer ordinary review questions: what authority does this code have, what can fail, what allocates, what is linear, and which claims are proved or merely checked? Every construct is accounted as one of: proved, enforced, reported, assumed, or trusted.
Trimmed --report audit output for the program above:
$ concrete main.con --report audit
--- Authority ---
read_u16_be : (pure)
report : Console
main : Console
--- Effects ---
read_u16_be
caps: (pure) alloc: none ffi: no trusted: no evidence: enforced
report
caps: Console alloc: none ffi: no trusted: no evidence: enforced
Totals: 3 functions, 1 pure, 0 allocating, 0 cross FFI, 0 trusted
Evidence: 0 proved, 3 enforced, 0 trusted-assumption, 0 reportedFull output and the other report modes are described in Reports.
What Concrete is not
- Not Rust with smaller syntax: Concrete rejects lifetime syntax and implicit drop.
- Not Zig with proofs bolted on: authority and allocation are part of reports.
- Not a GC language: ownership and cleanup stay visible.
- Not a proof assistant as a programming language: proof is evidence for systems code.
- Not a batteries-included platform: the standard library grows from workloads.
Influences
Concrete borrows restraint from Hare, allocator explicitness from Zig and Odin, result-oriented error style from Rust and Go, assurance discipline from SPARK/Ada, and kernel-checked evidence from Lean. The combination is stricter than any one source: no hidden authority, no hidden allocation, no hidden cleanup, no hidden proof class.