Concrete Spec

This page is the living language overview and design reference for Concrete.

It exists for a different job than the essays in the series. The series argues for the design. This page records the language shape, constraints, and current implementation status in one place.

If you want the shorter editorial introduction, read Why Concrete Exists.

Status

Concrete is real, but incomplete.

Today the project has:

What it does not yet have:

Design Principles

Concrete is organized around a few hard constraints:

  1. Pure by default.
  2. Explicit capabilities for effects.
  3. Linear ownership by default.
  4. No hidden control flow or hidden cleanup.
  5. A grammar small enough to parse with one token of lookahead.
  6. A language small enough that reports and proofs stay tractable.

Compilation Pipeline

The current compiler pipeline is:

Source
  -> Parse
  -> Resolve
  -> Desugar
  -> Check
  -> Elab
  -> CoreCanonicalize
  -> CoreCheck
  -> Mono
  -> Lower
  -> SSAVerify
  -> SSACleanup
  -> EmitSSA
  -> clang / linker

EmitSSA produces LLVM IR, which clang compiles and links into a native binary. There is also a built-in interpreter as an alternative execution path, useful for running programs without a native toolchain and for cross-checking the backend.

The architectural point is that Concrete has a real semantic boundary at Core IR and a real backend boundary at SSA. Core IR that passes CoreCheck is a validated artifact: downstream passes may assume its invariants hold, and the proof tooling attaches there. That keeps the compiler easier to reason about.

Types

Concrete includes:

The shape is conventional on purpose:

struct Copy Player { points: Int }

enum MyResult {
    Ok { value: Int },
    Err { error: Int },
}

trait Scorer {
    fn score(&self) -> Int;
}

impl Scorer for Player {
    fn score(&self) -> Int { return self.points * 2; }
}

fn evaluate<T: Scorer>(entity: &T) -> Int {
    return entity.score();
}

Copy appears in the type declaration itself, so whether a type is linear or freely copyable is visible at the definition site. Enum values are taken apart with match, which must be exhaustive:

match r {
    MyResult::Ok { value } => { return value; },
    MyResult::Err { error } => { return error; },
}

The standard library direction is intentionally ordinary rather than magical. The goal is to shrink compiler-known surface area over time and keep more user-facing behavior in regular library code.

Linearity

Owned values are linear by default. A linear value must be consumed exactly once.

That means:

Cleanup is explicit:

let f = open("data.txt")
defer destroy(f)

This is stricter than Rust’s affine ownership. The goal is visibility: resource lifetime becomes part of the program rather than hidden behind implicit Drop behavior.

Copy is explicit and opt-in. A type can only be Copy if all of its fields are Copy and it has no destructor obligations.

Borrowing

Borrowing lets code use a value without consuming it, while preserving linear ownership of the underlying resource.

Instead of Rust-style lifetime inference, Concrete uses scoped borrow blocks. A borrow block names the reference and names the region it lives in:

borrow owner as r in Region {
    // r: &T is available here; owner is frozen
}
// owner is usable again; r no longer exists

borrow mut owner as r in Region {
    // r: &mut T; exclusive access
}

While the block is active, the owner is frozen: it cannot be read, moved, or borrowed again. On block exit the owner thaws and the reference ceases to exist.

The broad rules are:

Concrete keeps this model intentionally lexical and explicit. It avoids signature-level lifetime machinery entirely, with no lifetime parameters and no elision rules, but it does so by accepting a smaller language surface.

Capabilities

Capabilities are static permissions declared on functions.

Examples:

fn read_file(path: String) with(File) -> String
fn serve() with(Network, Alloc, Console) -> Int
fn hash(data: &Bytes) -> Digest

A function with no capability annotation is pure. A function that allocates must declare with(Alloc). A function that touches files must declare with(File).

The current concrete capability set is: File, Network, Clock, Env, Random, Process, Console, Alloc, and Unsafe. Std is a macro for the standard safe capabilities, and user-defined capability aliases expand before the rest of the compiler sees them.

Capabilities propagate transitively through the call graph. If f calls g, and g requires File, then f must also require File.

This makes capabilities a real public contract rather than a documentation convention.

Allocation

Allocation is treated as a first-class effect.

If code allocates on the heap, it requires with(Alloc). Allocator choice is bound at the call site rather than hidden globally.

That gives you two properties that most languages do not expose cleanly:

Stack allocation does not require Alloc.

Trust Model

Concrete separates low-level trust boundaries instead of collapsing them into one broad keyword.

This separation matters because “does pointer tricks internally” and “can call arbitrary foreign code” are not the same kind of risk.

Errors

Errors are values. Concrete uses Result<T, E> with ? propagation:

fn read_config(path: String) with(File) -> Result<Config, FsError> {
    let f = open(path)?;
    defer destroy(f);
    return parse(f);
}

There are no exceptions and no hidden unwinding paths.

defer runs on normal scope exit, including early returns triggered by ?.

Abort is separate and immediate. It is outside normal cleanup semantics.

Contracts and Proofs

Functions can carry source-level contracts:

#[requires(0 <= n && n < 32)]
fn rotr(x: u32, n: u32) -> u32 {
    return (x >> n) | (x << (32 - n));
}

A contract is a claim, not a guarantee. The compiler turns each claim into proof obligations with stable ids, then attaches evidence. Preconditions are assumed at function entry and pushed to every caller; postconditions become exit obligations. Loops take explicit invariants and variants.

Evidence is tiered rather than binary. An obligation can be:

The audit report shows the evidence class for every obligation. There is never a single green badge.

concrete prove generates a Lean proof workspace for a function, links registered theorems back to their obligations, and supports replay so proofs stay tied to the source they were written against.

This is the part of the language that connects the essays’ argument to running code: the compiler does not just accept programs, it emits the facts about them that a proof can attach to.

Traits, Modules, and FFI

Traits are static dispatch only. The language avoids trait objects and most of the implicit machinery that tends to make systems languages harder to read and harder to formalize.

Modules use explicit imports and visibility. Imports name every symbol they bring in; everything is private unless marked pub:

import std.fs.{ open, FsError };

FFI exists, but it is deliberately narrow. extern fn declarations require FFI-safe types (integers, floats, Bool, Char, raw pointers, and C-layout structs), and foreign boundaries are tracked explicitly through the trust model:

extern fn malloc(size: u64) -> *mut u8;

Anti-Features

Concrete intentionally avoids a number of familiar features:

These are not omissions born of neglect; they are design constraints chosen to keep the language explicit, auditable, and mechanically tractable.

What You Can Say About Programs

If Concrete’s checker accepts a function, you can often say more than “it type-checks.”

Depending on the function, you may be able to say:

That is the main point of the language.

Open Questions

Several important areas are still intentionally unfinished:

Concrete is not trying to hide that incompleteness. The design and the implementation are meant to converge over time.