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:

• a full Lean 4 compiler pipeline from parse through SSA and native code generation
• strict LL(1) parsing
• structured diagnostics across semantic passes
• capability tracking and audit reports
• explicit IR boundaries, including Core and SSA
• a built-in test runner
• a growing low-level standard library

What it does not yet have:

• a fully formalized kernel connected end to end to the implementation
• verified elaboration and code generation
• mature tooling such as a formatter, package manager, and LSP

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
  -> Check
  -> Elab
  -> CoreCanonicalize
  -> CoreCheck
  -> Mono
  -> Lower
  -> SSAVerify
  -> SSACleanup
  -> EmitSSA
  -> clang / linker

The architectural point is that Concrete has a real semantic boundary at Core IR and a real backend boundary at SSA. That keeps the compiler easier to reason about and creates a plausible place to attach proof tooling.

Types

Concrete includes:

• primitive scalars such as Bool, integer types, floats, Char, String, and Unit
• records via struct
• algebraic data types via enum
• generic types and traits
• raw pointers for low-level and FFI work
• references via &T and &mut T

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:

• forgetting a value is a compile error
• using a value after move is a compile error
• destroying a value twice is a compile error

Cleanup is explicit:

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

This is stricter than Rust’s affine ownership. The point is not elegance. The point is that resource lifetime becomes visible in 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.

The broad rules are:

• while a value is borrowed, the owned value cannot be used incompatibly
• immutable borrows can coexist
• mutable borrows are exclusive
• references cannot escape their valid region

Concrete keeps this model intentionally lexical and explicit. It avoids a large amount of signature-level lifetime machinery, 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).

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:

• allocation can be audited semantically
• allocator strategy is explicit in the program structure

Stack allocation does not require Alloc.

Trust Model

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

• Capabilities express semantically visible effects.
• trusted fn and trusted impl mark pointer-level internal unsafety behind a safe API.
• trusted extern fn is a narrow carve-out for audited foreign bindings.
• with(Unsafe) marks foreign or semantically dangerous boundaries.

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.

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.

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.

FFI exists, but it is deliberately narrow. extern fn declarations require FFI-safe types, and foreign boundaries are tracked explicitly through the trust model.

Anti-Features

Concrete intentionally avoids a number of familiar features:

• garbage collection
• hidden allocation
• implicit destruction
• exceptions
• closures
• trait objects
• operator overloading
• reflection and eval
• implicit global state
• variable shadowing
• undefined behavior in safe code

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:

• it is pure
• it cannot allocate
• it cannot reach the network
• its trust boundaries are explicit
• its cleanup sites are visible
• it belongs to the proof-eligible fragment

That is the main point of the language.

Open Questions

Several important areas are still intentionally unfinished:

• concurrency model
• proof connection from Core IR to Lean theorems over user programs
• long-term verified kernel boundary
• mature tooling around formatting, packages, and editor support

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