Lain is a systems language in which memory safety, resource safety, integer safety and termination are proven at compile time and therefore not checked at runtime. A program that could read out of bounds, overflow, divide by zero, use a moved value or leak a resource does not compile.

Rejecting programs is only half of it. Every proof is also a fact the backend can use: exclusive access becomes restrict, an empty effect set becomes const, a declared length becomes access. And a check shown to be unnecessary is simply never emitted, including checks no optimiser could have removed on its own.

 your.ln ──▶ front end ──▶ Lain-IR ──▶ analyses ──▶ backend ──▶ executable
                          typed SSA    ownership     C99
                           and CFG     borrows       LLVM
                                       bounds
                                       overflow
                                       termination
                                       effects

Every analysis runs on the IR. None of them looks at the source text or at the output target, so the same proofs hold whichever backend emits the code.

Since 2026-09-17 that is also what a plain compile runs. Ownership, linearity, borrows, definite assignment, bounds, overflow, division and termination are all answered by the IR. The older AST engine was deleted on 2026-09-23.

Guarantees

	C / C++	Rust	Lain
Out-of-bounds read/write	UB	Panics at runtime	Rejected at compile time
Integer overflow	UB (signed)	Panics in debug, wraps in release	Rejected at compile time
Division by zero	UB	Panics	Rejected at compile time
Use after free / move	UB	Prevented	Prevented
Double free	UB	Prevented	Prevented
Resource leak	Silent	Allowed (mem::forget is safe)	Rejected
Dangling reference	UB	Prevented	Prevented
Uninitialised read	UB	Prevented	Prevented
Non-termination	Allowed	Allowed	Rejected in func
Data races	UB	Prevented	Single-threaded before 1.0
Array length in the type	No	Const generics only	a i32[out.len], a i32[h*w]
Aliasing told to the optimiser	manual restrict, UB if wrong	noalias from &mut	Derived from the borrow proof
Sum-type layout	manual	Niche packing, silent	Niche packing, and it warns when it fails

Against the C tooling, five minimal programs, one per error class, put through each tool in turn. Every one of them is undefined behaviour or a real leak in C, not merely something Lain dislikes:

Error class	gcc -Wall	gcc -fanalyzer	clang -Wall	ASan + UBSan	Valgrind	Lain
Use after free	warning	warning	missed	at runtime	at runtime	compile time
Resource leak	missed	missed	missed	missed	missed	compile time
Double free	warning	warning	missed	at runtime	at runtime	compile time
Buffer overflow	missed	warning	warning	at runtime	missed	compile time
Division by zero	missed	missed	missed	at runtime	missed	compile time

A warning does not stop the build, and the two runtime columns only report a bug on a run that actually reaches it. Measured with gcc 13.3, clang 18.1 and valgrind 3.22.

Contents

  1  Proof Engine
  2  Linear Type System
  3  Borrow Checking
  4  Value Range Analysis
  5  Termination Analysis
  6  Effect System
  7  Data Layout
  8  Code Generation
  9  Limits
 10  Quick Start

---

1. Proof Engine

The program below searches a slice of bytes for a value. The slice length is not known when the program is compiled, so every access into it has to be justified against a number that only exists at runtime.

func find(haystack u8[], target u8) usize {
    var i usize = 0
    while i < haystack.len {
        if haystack[i] == target { return i }
        i = i + 1
    }
    return haystack.len
}

Step 1. Lower to a typed SSA/CFG IR. Lowering attaches every safety obligation to a specific instruction. elem_ptr has to be shown in bounds, add has to be shown not to overflow, and the back edge into a loop header has to be shown to terminate.

Step 2. Work out what the values can be. Facts are propagated through the graph, and each loop is walked again until a pass adds nothing new, so what comes out holds on every iteration rather than only the first.

Two kinds of fact are kept: the range a value can take, and how two values compare. The second is what settles an array access. A range for i is no use when the length is unknown too, but i being below the length is enough whatever either turns out to be.

--dump-octagon prints what the compiler settled on at the array access:

── octagon state: bytes_find ──
  bb2
      %0:haystack ∈ [1, +inf]
      %2:i ∈ [0, +inf]
      %5 ∈ [1, +inf]                                   ; haystack.len
      …
      %2:i − %5 ≤ -1                                   ; the guard, carried in
      %4 − %5 ≤ -1
      …
    · %7 ∈ [0, +inf]   %7−%0:haystack≤-1   %7−%2:i≤0   %7−%4≤0   %7−%5≤-1

A value that came from a named local prints as %2:i; the unnamed ones are temporaries, and %5 is the one holding haystack.len.

Read the last line. %7 is the index, so %7−%5≤-1 says the index is at least one below the length. Neither value is known at compile time. The comparison between them is, and that is enough to settle the bounds check before the program runs.

Step 3. Check each obligation against those facts.

  find      index bounds   @ 4:13  PROVEN check-free
  find      arith overflow @ 5:4  PROVEN check-free
  find      termination    @ 0:0  PROVEN check-free
3/3 proof obligations discharged check-free

Step 4. Emit C, keeping what was proved.

__attribute__((pure)) __attribute__((nonnull))
size_t bytes_find(size_t __len_haystack, const uint8_t * restrict haystack, uint8_t target) {
    size_t i = 0;
    while (i < __len_haystack) {
        if (haystack[i] == target) {
            return i;
        }
        i = i + 1;
    }
    return __len_haystack;
}

Nothing in the Lain source asked for pure, nonnull or restrict, and nothing asked for the length to be passed separately. Each one is a fact the analyses established.

Change < to <= and the fact becomes %7 − %5 ≤ 0. The index can now equal the length, so the bounds obligation no longer holds and the program is rejected — twice:

[E085] Error Ln 4, Col 12: index is not provably within bounds
  --> bytes.ln:4:12
   |
 4 |         if haystack[i] == target { return i }
   |            ^
[E086] Error Ln 5, Col 13: arithmetic is not provably free of overflow
  --> bytes.ln:5:13
   |
 5 |         i = i + 1
   |             ^

The second is not noise, and it is the more interesting of the two. Once i may reach the length, nothing bounds it any more, so at the maximum length i = i + 1 can overflow — a separate obligation, broken by the same character.

The analyses in the chapters below depend on one another. Because the borrow checker guarantees a mutable borrow is exclusive, the numeric analysis can keep a fact about a value across a function call. Because the effect system knows a function cannot panic, the backend is allowed to mark it const.

---

2. Linear Type System

Linear types (Girard, 1987; Wadler, 1990) require a value to be used exactly once. Rust is affine: a value is used at most once, which is why leaking is safe there. Lain is linear, so using a value zero times is an error as well.

Using it twice is rejected:

type Buffer {
    mov data *u8
    len usize
}
func release(mov {data, len} Buffer) { }

func main() i32 {
    var p *u8 = 0
    var b = Buffer(p, 0)
    release(mov b)
    release(mov b)          // E002: 'b' was already used/consumed
    return 0
}

and not zero:

type Buffer {
    mov data *u8
    len usize
}
func release(mov {data, len} Buffer) { }

func main() i32 {
    var p *u8 = 0
    var b = Buffer(p, 0)    // E003: linear field 'data' of 'b' was not consumed
    return 0
}

The rule applies per field, so a struct can be taken apart a piece at a time and each piece is tracked separately. It is flow-sensitive, so consuming a value on one branch but not the other is caught. defer counts as the consumer, and it counts at every exit from the function, including the exit taken when an error propagates out.

Rust accepts the second program. mem::forget is safe, Rc cycles leak, and Rust states that leaking is outside its guarantees.

---

3. Borrow Checking

The rule is one mutable borrow or many shared ones, never both, and a borrow ends at its last use rather than at the end of its scope. The regions come from Cyclone (Jim et al., 2002), the loan discipline from Patina (Reed, 2015) and Oxide (Weiss et al., 2019), and the last-use refinement from non-lexical lifetimes.

Two things follow from that beyond the safety property.

No lifetime annotations

Lain has no lifetime syntax. A function returning a borrow is written without one, and the compiler works out the relationship itself:

type Data { x i32 }

func pick_x(var a Data, var b Data) var i32 { return var a.x }

func main() i32 {
    var p = Data(1)
    var q = Data(2)
    var r = pick_x(var p, var q)
    r = 7
    return q.x
}

Rust rejects the same signature until a lifetime is written on it:

error[E0106]: missing lifetime specifier
2 | fn pick_x(a: &mut Data, b: &mut Data) -> &mut i32 { &mut a.x }
  |              ---------     ---------     ^ expected named lifetime parameter

The relationship is read out of the body, so the result is known to borrow a and not b, and b stays usable while the result is alive. Rust can express that too, but only if you write <'a, 'b> yourself: its own suggested fix ties both parameters to one lifetime and freezes b.

The pre-rebuild checker, deleted on 2026-09-23, assumed a returned borrow came from every mutable parameter. Move the write to q above the last use of r, so that the borrow is still live when q is touched, and that checker rejected the program with E004; the compiler accepts it, because it knows the borrow came from a.

Exclusive borrows become restrict

C's restrict is a promise that two pointers never refer to the same object, and the C compiler takes it on trust. In Lain that promise is the borrow checker's output, so it can be emitted.

Below is the same loop compiled twice. The only difference is whether restrict was passed through to gcc (-O3 -march=x86-64-v3):

func vadd(out var i32[], a i32[out.len], b i32[out.len]) {
    var i usize = 0
    while i < out.len {
        out[i] = a[i] +% b[i]
        i = i + 1
    }
}

; with the proof                          ; proof withheld
vadds_vadd:                               vadds_vadd:
  endbr64                                   endbr64
  test  %rdi,%rdi                           mov   %rdi,%r8
  je    cb                                  mov   %rdx,%rdi
  lea   -0x1(%rdi),%rax                     test  %r8,%r8
  cmp   $0x6,%rax                           je    11e
  jbe   d4                                  lea   -0x1(%r8),%rax
  mov   %rdi,%r8                            cmp   $0x2,%rax
  xor   %eax,%eax                           jbe   100          ─┐ to the scalar copy
  shr   $0x3,%r8                            lea   0x4(%rdx),%r9 │
  shl   $0x5,%r8                            mov   %rsi,%rdx     │ overlap test 1
                                            sub   %r9,%rdx      │
  vmovdqu (%rdx,%rax,1),%ymm1               cmp   $0x18,%rdx    │
  vpaddd  (%rcx,%rax,1),%ymm1,%ymm0         jbe   100          ─┤
  vmovdqu %ymm0,(%rsi,%rax,1)               lea   0x4(%rcx),%r9 │
  add     $0x20,%rax                        mov   %rsi,%rdx     │ overlap test 2
  cmp     %r8,%rax                          sub   %r9,%rdx      │
  jne     <loop>                            cmp   $0x18,%rdx    │
                                            jbe   100          ─┘
                                            ...
                                          100:                  ; the scalar copy
                                            mov   (%rcx,%rax,4),%edx
                                            add   (%rdi,%rax,4),%edx
                                            mov   %edx,(%rsi,%rax,4)
                                            add   $0x1,%rax

Both versions end up with an AVX2 loop. Only the left one goes straight into it. On the right gcc has to check at runtime whether the three buffers overlap, and has to keep a scalar copy of the loop to jump to when they do: 59 instructions against 81.

What that is worth depends on how long the loop runs, and it is worth being exact. The overlap test happens once per call, so it vanishes into a long loop and dominates a short one:

       n    restrict     without     ratio
       8      57.2 ms      72.6 ms    1.27x
      16      47.0 ms      61.8 ms    1.32x
      64      29.7 ms      31.9 ms    1.07x
     256      19.4 ms      19.4 ms    1.00x
    4096      38.4 ms      38.4 ms    1.00x

On long vectors gcc's runtime versioning recovers everything and the proof buys only smaller code. On the short ones that fill inner loops it is worth about a third. What does not vary with n is that in C you have to write restrict yourself, and it is undefined behaviour if you are wrong.

---

4. Value Range Analysis

This is abstract interpretation (Cousot and Cousot, 1977) using the octagon domain (Miné, 2006), which stores facts of the form ±x ±y ≤ c, widened against thresholds as in Astrée.

Storing comparisons between values, rather than only ranges, is what makes it useful on real code. The fact that makes an array access safe is hardly ever a constant. It is usually a comparison with a length that is itself unknown.

the access	proven by
scan a[i] under i < a.len	i − len ≤ −1, straight from the guard
two-pointer a[i] under i ≤ j < a.len	transitive closure: i − j ≤ 0 and j − len ≤ −1
reverse a[a.len-i-1]	len − i ≥ 1, from i < len
masked gather a[x & (N-1)], any x	x & (N−1) ∈ [0, N−1] for every x, no assumption on the data
sliding window a[i+1] over a i32[n] under i < n-1	the guard as i − n ≤ −2, so (i+1) − n ≤ −1
insertion sort a[j-1] under j > 0 ∧ j < a.len	offset by −1, lower bound from j > 0
2D a[i*w + j] over i32[h*w]	per dimension: i < h ∧ j < w
binary search a[lo + (hi-lo)/2] over a i32[8]	an inductive loop invariant recovers 0 ≤ lo < hi ≤ len, which the loop's blanket widening had thrown away, then mid < hi

Each row is a program in the test corpus. Since an index the compiler cannot place in bounds is an E085 rather than a runtime check, a program compiling is what tells you the bound was proved.

The last row is the current edge: binary search proves over a fixed-length array, and the same search over a runtime length is still rejected.

Lengths can be part of a type

A parameter's length can be written as an expression over the other parameters:

func vadd(var out i32[], a i32[out.len], b i32[out.len]) {
    for i in 0..out.len {
        out[i] = a[i] +% b[i]
    }
}

a and b are arrays the same length as out. Callers have to satisfy that, and are told so with E087 if they do not; inside the body it comes for free.

The addition wraps (+%) because the elements are unbounded i32 and their sum is a real overflow — the lengths being proven says nothing about the values. Writing + here is rejected: proving where a value lives says nothing about how large it is, and the two obligations are separate.

The expression can be anything, so a matrix is just a flat buffer with a shape. Here h and w are unknown at compile time and a[i*w + j] still needs no check. They are bounded because the declared length is itself arithmetic: h * w on two unbounded usizes overflows, and a bound needs a named parameter to attach to.

func msum(h usize < 4096, w usize < 4096, a i32[h * w]) i32 {
    var s i32 = 0
    var i usize = 0
    while i < h {
        var j usize = 0
        while j < w {
            s = s +% a[i * w + j]
            j = j + 1
        }
        i = i + 1
    }
    return s
}

C has no way to state that precondition. Rust's const generics cannot take h * w.

Wide accesses are checked at their real width

A 16-byte SIMD load has to satisfy i + 16 ≤ len, not i < len. That is still an ordinary comparison, so the same analysis handles it and there is no SIMD-specific reasoning anywhere in the compiler:

func scan(src u8[4096], n u32 < 4097, start u32 < 4097, term u8) u32 {
    var i u32 = start
    while (i + 15) in 0..src.len and i +% 16 <= n {
        var hit u32 = @movemask(@load(u8x16, src, i) == term) & (65535 as u32)
        if hit != 0 {
            i = i +% (@ctz(hit) as u32)
            break
        }
        i = i +% 16
    }
    while i in 0..src.len and i < n and src[i] != term { i = i +% 1 }
    return i
}

No unsafe. No runtime bounds check.

Arithmetic works the same way

+ widens its result, so adding two i32 values cannot overflow. What can fail is storing the result somewhere narrower, and that is where the check goes:

func widened(a i32, b i32) i64 { return a + b }     // accepted

func narrowed(a i32, b i32) i32 {
    var s i32 = a + b       // E086: the sum may not fit an i32
    return s
}

When overflow is what you want, say which kind: +% wraps, +| saturates, a +? b else 0 gives you a fallback value, and unsafe { } turns the check off. What you cannot do is leave the question unanswered.

Division is handled the same way, and the error lists the ways out:

[E015] Error: division/modulo by a divisor whose range [-2147483648, 2147483647]
       includes zero. Guard it (`if d != 0`), constrain it (`d int != 0`), or wrap
       the divide in an `unsafe` block.

Both of those are real. func divide(a i32, b i32 != 0) i32 puts the constraint in the signature, where every caller has to satisfy it, and an if b != 0 that dominates the division settles it locally.

Where no optimiser can follow

An optimiser can only use facts it can see. When the fact that makes an access safe lives at the call site, and the function is compiled separately, it is out of reach. Preconditions in Lain are part of the signature, so the caller discharges them and the callee is free of them:

func get(a i32[n], n usize, i usize < n) i32 {
    return a[i]
}

i usize < n is proven at every call site, at compile time. Inside, nothing is left to check, and the proof is handed on to gcc as an assumption. This is the emitted C for get.ln, with the local declarations left out. The slice arrives as its length and pointer, v1 is n and v2 is i:

__attribute__((pure)) __attribute__((nonnull)) __attribute__((access(read_only, 2, 1)))
int32_t get_get(size_t __len_v0, int32_t* restrict __ptr_v0, uint64_t v1, uint64_t v2) {
  Slice_i32 v0 = { __ptr_v0, __len_v0 };
 L0: ;
  v3 = v0.len;
  v4 = (v3 <= v1);
  v5 = (v3 >= v1);
  v6 = (v2 < v1);
  if (!(v4 & v5 & v6)) __builtin_unreachable();
  v7 = v0.data;
  v8 = &v7[v2];
  v9 = *v8;
  return v9;
}

The facts go to gcc as ONE conjoined condition, because gcc 13 ignores an unreachable-guard whose variable was already used by an earlier one. The assumption is not decoration. In a callee that loops, it removes the test for an empty loop that gcc would otherwise have to keep:

func dot(a i32[n], b i32[n], n usize >= 4) i32 {
    var s i32 = 0
    var i usize = 0
    while i < n {
        s = s +% (a[i] *% b[i])
        i = i + 1
    }
    return s
}

; without the hint (n unknown)   ; with `if (!(... & n >= 4)) __builtin_unreachable();`
dot_dot:                          dot_dot:
  endbr64                           endbr64
  test %r8,%r8                      xor  %eax,%eax
  je   <return 0>                   xor  %edi,%edi
  xor  %eax,%eax                  loop:
  xor  %edi,%edi                    mov  (%rsi,%rax,4),%edx
loop:                               imul (%rcx,%rax,4),%edx
  mov  (%rsi,%rax,4),%edx           ...

The same guarantee in C has to be a runtime check, because the callee cannot see who called it:

; Lain                          ; C: if (i >= n) abort();      ; Rust: a[i]
get_get:                        get_checked:                    get_rs:
  endbr64                         endbr64                         cmp  %rsi,%rdx
  mov  (%rsi,%rcx,4),%eax         cmp  %rsi,%rdx                  jae  <panic>
  ret                             jae  <abort>                    mov  (%rdi,%rdx,4),%eax
                                  mov  (%rdi,%rdx,4),%eax         ret
                                  ret                             ...panic landing pad

gcc and LLVM both keep their check, and neither is doing anything wrong: the information that would remove it is in another translation unit.

This is the honest shape of the advantage. Inside a single function an optimiser is often as good, when one loop counter explains the index. The masked index in the table above, a[x & 4095] over a 4096-element array, is proved by gcc and by LLVM as readily as by Lain. It is weaker when the bound is a relation between two variables that both move: rustc -O keeps a check on every iteration of a binary search, even over a fixed [i32; 64], and of a two-pointer scan. What an optimiser cannot do at all is carry a fact across a boundary it cannot see through, or reject the program when the fact does not hold.

---

5. Termination Analysis

A func always finishes. Every loop and every recursive call needs some quantity that shrinks on each step and cannot shrink forever, and in most cases the compiler works out what that quantity is: while i < n gives n − i, while i > 0 gives i, while lo < hi gives hi − lo.

The step does not have to be by one. Whether a quantity shrinks is something the numeric analysis already knows, so halving and shifting need nothing written:

func bits(x u32) u32 {
    var n u32 = x
    var c u32 = 0
    while n > 0 {           // measure `n` inferred; n/2 < n for n > 0
        n = n / 2
        c = c + 1
    }
    return c
}

Euclid's algorithm needs the quantity named, though not justified. Since b = a % b lands in [0, b-1], the divisor shrinks on every iteration:

func gcd(a0 usize, b0 usize) usize {
    var a usize = a0
    var b usize = b0
    while b > 0 decreasing b {
        var t usize = b
        b = a % b
        a = t
    }
    return a
}

Recursion is held to the same standard:

func factorial(n int) int {
    if n <= 1 { return 1 }
    return n *% factorial(n - 1)      // accepted: n shrinks toward the base case
}

func collatz(n int) int {
    if n <= 1 { return 0 }
    if n % 2 == 0 { return collatz(n / 2) }
    return collatz(3 * n + 1)         // E011: no decreasing measure
}

Termination is the default, and effects diverge is how a function opts out of it — the same clause that admits any other effect, so nothing here is special-cased:

extern func libc_putchar(c i32) i32 effects io

func serve(fd i32) effects io, diverge {
    while 1 { libc_putchar(fd) }
}

That row is not a suppression. It is a fact about serve that every caller inherits: a func with no diverge in its row cannot call it without saying so.

---

6. Effect System

Every function gets a set of effects drawn from {diverge, raises, io, alloc}, worked out by following the call graph. func is the only introducer and its default is the empty set, so a function that deviates says which way with effects … — one clause for the whole family:

extern func libc_malloc(n usize) mov *void effects io, alloc

func dup(n usize) mov *void effects io, alloc { return libc_malloc(n) }

func must_parse(ok bool) i32 effects raises {
    if ok { return 1 }
    panic("bad")
}

Silence means the empty set, and the row is a complete upper bound. Those are one rule read from two sides: an effect the body has and the row does not name is an error, so a caller can trust what it reads. Omitting the clause is the strongest claim, not the quietest one:

[E130] Error Ln 12, Col 6: 'talk' declares `effects` that do not cover what its body does —
       it also has: io.

An extern is the one place the rule inverts, for the one reason that it has no body: nothing can be inferred, so its row is BELIEVED, its default is every effect, and writing a row NARROWS it. Forgetting one on a C function that does I/O therefore costs precision, never soundness:

extern func libc_printf(fmt *u8, ...) i32 effects io    // believed; narrows
extern func abs(n i32) i32 effects                      // the empty row: genuinely pure

An empty effect set lifts a call out of a loop

A function with no effects writes no global state, does no I/O, allocates nothing and cannot panic. Its result depends on its arguments and nothing else, which is what __attribute__((const)) claims in C.

A compiler that knows this can move the call. If the arguments do not change inside a loop, neither can the result, so the call belongs outside it:

func scale(x i32, y i32) i32 {
    var a i32 = (x *% 2654435761) ^ (y *% 40503)
    a = a ^ (a >> 13)
    return a *% 1274126177
}

func apply(out var i32[], p i32, q i32) {
    var i usize = 0
    while i < out.len {
        out[i] = out[i] +% scale(p, q)
        i = i + 1
    }
}

scale has no effects, so it is declared to the C compiler as const:

__attribute__((const)) int32_t licm_scale(int32_t, int32_t);

Compiled separately, so the annotation is all gcc has to go on:

; effect set known                       ; effect set withheld
licm_apply:                              licm_apply:
  ...                                      ...
  call  <licm_scale>   ; once, here      <loop>:
<loop>:                                    mov   (%r15,%rbx,4),%ebp
  add   %eax,(%rdx)    ; reuse result      mov   %r14d,%esi
  add   %eax,0x4(%rdx)                     mov   %r13d,%edi
  add   $0x8,%rdx                          call  <licm_scale>   ; once per element
  cmp   %rcx,%rdx                          add   %eax,%ebp
  jne   <loop>                             mov   %ebp,(%r15,%rbx,4)
                                           add   $0x1,%rbx
                                           cmp   %rbx,%r12
                                           jne   <loop>

On the left the call happens once, before the loop starts, and the loop reuses the value in %eax. On the right it happens on every iteration: over a 4096-element array that is 4096 calls instead of one.

Written by hand in C, const is a claim nobody verifies. Here it is the effect set, which the compiler worked out.

Panics are tracked for a specific reason. const also lets gcc delete a call whose result is never used, so putting it on a function that can abort turns a program that aborts at -O0 into one that runs clean at -O3. This project shipped that miscompile once, and treating a panic as an effect is what fixed it.

The row is only as good as its weakest check

It shipped a second time, by a different route, and the second one is the more useful story. A function pointer carries a row, so a call through it is charged the arrow's row — on the premise that the row was checked wherever the pointer got its value. That check existed in one place: a var initialiser. Reach the pointer any other way and nothing looked:

// ERROR: [E122] the function may do more than the arrow admits
extern func libc_printf(fmt *u8, ...) i32 effects io

type S { cb *func(i32) i32 }

func noisy(n i32) i32 effects io {
    libc_printf("side effect\n")
    return n
}

func run(s S) i32 {
    return s.cb(0)
}

func main() i32 effects io {
    var s = S(noisy)
    unused = run(s)
    return 0
}

run reaches an io function, through a field whose arrow claims none. Before this was fixed the program compiled, and run was emitted __attribute__((pure)) — a promise to the C compiler that calling it twice is the same as calling it once, and that a call whose result is unused may be dropped. The interpreter, which runs the program on the IR's own semantics, prints the side effect. gcc is entitled to delete it, and with this gcc it did:

build	times the side effect printed
lain --interpret	1
gcc -O0	1
gcc -O1	0
gcc -O2	1

The -O2 row is why this kind of bug survives. Nothing is promised about which optimiser at which level takes the permission — gcc 13 inlined the call at -O2 and kept the effect, and deleted it at -O1. A wrong annotation does not reliably break anything. It breaks something occasionally, on one compiler, at one level, which is indistinguishable from a flake until someone reads the emitted C.

The fix is not another check at another site. The row is now verified wherever a value takes a function-pointer type, by one check that every such boundary passes through — an initialiser, an assignment, a return, a call argument, a struct constructor, a sum payload, an array element. Two instances of one wrong annotation, arriving by different routes, is what makes that the right shape: an annotation derived from an analysis is only as sound as the weakest place that analysis is consulted.

---

7. Data Layout

A sum type whose payload has spare bit patterns is laid out without a tag. Option(*u8) is one pointer, with None as the null pointer:

type OptionByte {
    Some { v *u8 }
    None
}

This is the C lain emits for it, compiled as ob.ln (the module name prefixes each function) with two one-line functions added, func some(p *u8) OptionByte { return OptionByte.Some(p) } and its None twin:

typedef uint8_t* OptionByte;

__attribute__((pure)) OptionByte ob_some(uint8_t* v0) {
  OptionByte v1;
 L0: ;
  v1 = (OptionByte)v0;
  return v1;
}

__attribute__((const)) OptionByte ob_none(void) {
  OptionByte v0;
 L0: ;
  v0 = (OptionByte)(uintptr_t)0ull;
  return v0;
}

Rust does this too, and calls it the same thing. Errors get the same treatment, so *u8 | NotFound | Denied is still one pointer wide, with the two error cases at addresses 0 and 8 where no real object can sit. No tag word, no allocation, no unwinding.

The difference is what happens when it does not fit. For a union whose error cases carry no payload, the packing is not an optimisation the compiler attempts. It is required, and the program is rejected when it cannot be done:

// ERROR: [E064] the union cannot be zero-cost — i32 has no spare values
func get(flag bool) i32 | NotFound | Denied {
    if flag { return 1 }
    return NotFound
}

[E064] Error: the union `i32 | ...` cannot be zero-cost: the value type has 0 spare
       values, and 2 payload-less variants need one each. Give the value type spare
       values (a pointer, a bool, or a refined alias like `type Small = u8 < 200`), or
       use fewer markers.

The remedy it names works, and it costs nothing: give the value type spare values by naming a refined alias, and the same three-way union is one byte, with both error cases stored in values the alias rules out:

// VERIFY: exit 0
type Small = u8 < 200

func get(flag bool) Small | NotFound | Denied {
    if flag {
        var v Small = 1
        return v
    }
    return NotFound
}

func main() i32 {
    if @sizeof(Small | NotFound | Denied) != 1 { return 1 }
    return 0
}

The alias is what makes it work. A refinement cannot be written inline where a union's value type goes, so u8 < 200 | NotFound is not a type; Small | NotFound is.

That is a deliberate trade, and it cuts both ways: a program that would have compiled elsewhere does not compile here. Where a tag is genuinely unavoidable, because an error case carries a payload, it is allowed and reported rather than added quietly:

type FileErr { NotFound, Permission, Oom }
type R { Ok { p *i32 }, Err { e FileErr } }

func f() R {
    return R.Err(FileErr.Oom)
}

[W120] Warning: enum 'R' is not zero-cost: it carries a uint8_t tag (1 byte) beside its payloads.
       It does because 2 of its variants carry a payload, and only a sum with ONE payload-carrying variant can store the others in the payload's spare values.

A layout optimisation that quietly fails is a cost you find later with a profiler. This one is either guaranteed or refused, and says which.

An enum that declares its width is a niche source

A plain enum has no spare values the layout can use, because nothing says how wide it is. Declare the width and the values above the last variant become spare, which is enough to pack an option over it into a single byte:

type K u8 { A, B, C }

type Opt {
    Some { k K }
    None
}

func main() i32 {
    assert @sizeof(Opt) == 1
    o = Opt.Some(K.B)
    return case o {
        Some(k): 0
        None: 1
    }
}

K occupies 0, 1 and 2, so None is stored as 3 and the sum needs no tag. Without the u8 the same program compiles and warns, naming the fix:

type P { A, B, C }

type Opt2 {
    Some { p P }
    None
}

func main() i32 {
    o = Opt2.Some(P.B)
    return case o {
        Some(p): 0
        None: 1
    }
}

[W120] Warning: enum 'Opt2' is not zero-cost: it carries a uint8_t tag (1 byte) beside its payloads.
       It does because the payload of 'Some' has 0 spare values, and 1 payload-less variant needs one.
       To drop the tag, declare the width of 'P' (`type P u8 { ... }`): its values above the last variant are then spare.

There is one exception, and it is about C rather than about Lain. If an extern signature can reach the enum — as a parameter, a result, or through a pointer, a struct or a function pointer — the tag stays, because C is free to hand back any value of that width and none of them is reliably spare:

type K u8 { A, B, C }

extern func takes_k(k K) i32 effects

type Opt3 {
    Some { k K }
    None
}

func main() i32 {
    o = Opt3.Some(K.B)
    return case o {
        Some(k): takes_k(k)
        None: 1
    }
}

[W120] Warning: enum 'Opt3' is not zero-cost: it carries a uint8_t tag (1 byte) beside its payloads.
       It does because its payload is the enumeration 'K', which an extern's signature reaches, so C may hand it any value of its width and none is spare.

A value of an enumeration type is always one of its variants; writing anything else into its storage is undefined behaviour, which is what makes the spare values usable in the first place.

---

8. Code Generation

What the C compiler is told

Here is a nine-line sliding-window sum over a runtime length. Its Lain source carries no annotations at all. This is the declaration it produces:

__attribute__((access(read_only, 1, 2)))
__attribute__((pure))
__attribute__((nonnull))
int32_t window(const int32_t * restrict a, size_t n);

Five separate facts about the function, none of them written by the programmer:

C annotation	Derived from	What it is in C
restrict	The borrow checker rejects any program where two reference parameters could name the same object	A claim the C compiler trusts. UB if wrong
access(read_write, n, m)	The declared length: parameter n holds m elements	A claim the C compiler trusts
const T *	The set of things the function writes, computed from its body	Not checked across the call
pure / const	An empty effect set: no writes, no I/O, no allocation, no panic	A claim the C compiler trusts. If it is wrong, calls that had to happen get deleted
nonnull	A borrow can never be null	A claim the C compiler trusts

Targets

C99 is the backend that works. It compiles the whole corpus, and every listing on this page came out of it. The output is portable and readable, and ordinary debuggers understand it.

There is also an LLVM path, and it is a demonstration rather than a backend. --emit-llvm lowers integer functions built from + - *, the comparisons, if and return, and passes the proved ranges through as @llvm.assume — which is where more of the value eventually is, since it reaches optimisations that going through C cannot express at all.

Outside that subset it now refuses, and it did not always. It used to emit a comment and carry on, which sounds harmless and was not: return a +% b came out as add i32 %a, 0, so the function returned a. Wrong output that looks like valid LLVM IR, from a compiler whose whole claim is prove-or-reject — and measured across the corpus, 120 of 120 programs contained at least one such placeholder. It reports what it cannot model and translates nothing, the same way the C backend refuses a construct it has not modelled.

So C is the path that runs, and the honest summary of the LLVM one is that the seam exists and the backend does not.

Neither target owns the proofs. They are settled on the IR, which is why adding a backend is ordinary work rather than a redesign.

---

9. Limits

• A running total with no bound is rejected, not checked. This is the rule that will cost you the most, and it is worth seeing why it has to be one:

  func up8(n u8) u8 {
      var s u8 = 0
      var i u8 = 0
      while i < n {
          s = s + i          // ERROR: [E086] this running total can overflow the type
          i = i + 1
      }
      return s
  }
  

  Until 2026-09-17 that compiled, and up8(200) printed 188 instead of 19900. A total's bound is start + trips × step, which is a PRODUCT — not something a relational domain can hold — so the engine asks you to bound one of the three: the count (a length with a refinement, f(a i32[n], n usize < 4096), or a counter that falls by a fixed step, which runs at most its start divided by the step), the element (a narrower type, or a refinement on it), or the total (a wider accumulator, widening the addend too). Or say which arithmetic you meant: +% wraps, +| saturates. The diagnostic names all four.

  Bounding the element is the one that reads best, and it needs no new syntax — a refinement ALIAS is an element type:

  type Small = i32 >= 0 and <= 1000
  
  func total(a Small[64]) i32 {
      var s i32 = 0
      var i usize = 0
      while i < 64 {
          s = s + a[i]          // proves: 64 x 1000 = 64000, which fits i32
          i = i + 1
      }
      return s
  }
  

  The emitted C for total contains no check, no trap and no branch on the index, and gcc receives it as __attribute__((pure)) __attribute__((nonnull)). Widen Small to <= 100000000 and the same function is refused again — the bound is multiplied by the trip count, not merely noted. And the bound is enforced where the values are produced: storing 5000 into a Small element is [E086], at construction, at a later store, and through a var parameter.

• No concurrency. Single-threaded before 1.0, so "no data races" is a consequence of that rather than something achieved. An interrupt-aware model is planned.

• unsafe turns off the numeric and bounds checks inside it. It is a block, so it is easy to find.

• Generics are monomorphised with no trait bounds. Mistakes show up when a generic is instantiated rather than where it is defined.

• A fact relating three quantities at once is outside the octagon by construction. The domain holds x ± y <= c with a constant on the right, so a window checked as , or an allocator's , cannot be proven, and the sum is refused before that, since it can overflow:

---

10. Quick Start

make                                                     # build the compiler
./lain my_program.ln -o out.c                            # Lain  -> C99
gcc out.c -o my_program -Dlibc_printf=printf -w          # C99   -> executable

Run from the repository root if a program imports from std/, since module paths are resolved relative to the working directory, not to the source file. lain sub/prog.ln looks for std/math.ln under the directory you are standing in, not under sub/.

USAGE.md is the compiler's manual: every flag, the exit codes, why -Dlibc_printf=printf and -w are needed, how to run a program on the IR's own semantics instead of emitting C, and how to read a diagnostic.

make test                # the corpus
make gates               # the corpus, the examples on this page, the spec, the IR units
make fuzz                # the fuzzers: they run what the compiler claimed was safe

scripts/gates/readme_gate.sh pulls every Lain example off this page and compiles it. Examples labelled with an error have to fail; the rest have to compile. It exists because the previous version of this file spent months describing a language the compiler had stopped implementing.