Language Invariants

Status: stable reference

These rules apply across all phases. They come directly from the language design and must never be violated.

1. Authority-Free By Default

A function without with() cannot exercise capabilities or call a function whose required capability set is non-empty. This is an authority claim, not a totality claim: such a function may still trap on a checked operation, diverge, or exhaust the stack. Proof eligibility and stronger behavioral claims are separate judgments.

2. True Linear Types

Every linear value must be consumed exactly once. Not zero (leak = compile error). Not twice (double-use = compile error). Forgetting a resource is rejected.

What counts as consuming a value

Passing it as a by-value argument to a function or method (including destroy(x))
Returning it from a function (return x)
Moving it into a struct field during construction (Point { x: val })
break val inside a loop-as-expression
Destructuring via match or let (the original is consumed, the fields become new bindings)
Storing into an array element during array literal construction ([val1, val2])

Each phase that adds a new consumption form must update this list.

What does not count as consumption

borrowing (&x, &mut x)
taking an address for a raw pointer (&x as *const T)
deferring (defer destroy(x) reserves but does not consume until execution)

3. No Hidden Control Flow

a + b on integers is primitive addition, not a method call. The compiler never inserts destructor calls — you write defer destroy(x) explicitly. If it allocates, you see with(Alloc). Errors propagate only where ? appears.

Note on `defer`

defer schedules code at scope exit, but the programmer writes defer explicitly at the point of scheduling. The compiler emits the deferred call at the point of scope exit. This does not violate the invariant because:

the programmer wrote the defer statement
the execution point (scope exit) is deterministic and visible from the block structure
no implicit function dispatch occurs; the exact function being called is the one written in the defer statement

4. No Lexical Value Shadowing

Status: decided language invariant; enforcement pending ROADMAP R-0435. Until that task lands, this section distinguishes the target rule from current compiler behavior.

Target rule: a new local value binding may not reuse the spelling of another local value binding visible along its lexical scope chain. Parameters, let, pattern and loop binders, and borrow-block value/region binders all introduce names. let s = transform(s) is therefore rejected as a new binding.

Assignment does not introduce a binding. acc = f(acc, x) remains legal for a mut linear place once evaluation consumes its old value; assigning over a live linear value remains E0219. Sibling match arms may use the same spelling because their bindings are not visible to one another. The rule is confined to lexical value bindings; fields, types, traits, modules, top-level functions, imports, and intrinsics are separate namespaces.

Current compiler behavior: ordinary let/pattern shadowing is still accepted except for a still-live non-Copy binding and borrow-block ref/region collisions. Elaboration must continue to preserve binding identity even after the source restriction lands.

5. No Uninitialized Variables

All variables must be initialized at declaration.

6. No Operator Overloading

Operators (+, -, *, /, %, ==, !=, <, >, <=, >=, &&, ||, !) on primitives (Int, Uint, i8-i64, u8-u64, f32, f64, Bool) are built-in. They are not trait method calls. User-defined types cannot use these operators — use named functions instead.

7. No Implicit Conversions

No silent coercion between types. Explicit as casts only.

8. No Null

Optional values use Option<T>.

9. No Exceptions

Errors are values (Result<T, E>), propagated with ?.

10. No Global Mutable State

All global interactions are mediated through capabilities.

11. No Interior Mutability In Safe Code

All mutation flows through &mut. Exception: UnsafeCell<T> in later low-level stdlib work, gated by Unsafe. Before that, interior mutability does not exist in safe code.

12. Local-Only Type Inference

Function signatures must be fully annotated. Inside function bodies, local variable types may be inferred from the right-hand side of let bindings.

Inference direction:

right-to-left only
no cross-statement constraint solving
no broad bidirectional inference

13. LL(1) Grammar

Every parsing decision must be possible with a single token of lookahead. No ambiguity, no backtracking.

14. Readability Is Part of Correctness

Surface syntax, stdlib APIs, and trusted boundaries should stay explicit enough that ordinary code can be read and audited predictably. A feature that makes low-level behavior harder to see increases audit cost and should be treated as a correctness concern, not merely a style issue.

15. New Features Must Justify Their Cost

New language features must justify:

grammar cost
audit cost
proof cost

If a feature makes the language harder to parse, harder to review, or harder to prove without delivering a correspondingly large benefit, it should be rejected or delayed.

16. `abort()` Is Terminal And Runs No Cleanup

Deferred cleanup, explicit Destroy calls, and generated drop glue do not run after abort(). In the current hosted profile, abort terminates the process. A future freestanding profile must route it to a declared non-returning target handler. Neither profile promises cleanup or recovery; ROADMAP R-0223 and R-0322 own the full runtime/target contract.

On POSIX systems, abort() typically produces exit code 134, but tests should check for nonzero exit rather than a specific code.

17. Reproducible Builds

Same source plus same compiler should yield the same binary. No timestamps, random seeds, or environment-dependent output.

18. Diagnostics Stay Structured

The compiler keeps diagnostics structured through the main semantic pipeline. It may accumulate multiple errors across functions or modules, but it does not rely on broad recovery or ambiguous parse fallback to continue.