# Language-design constraints (binding)

## Language-design constraints (binding)

The four constraints below are necessary preconditions for RC to
be sound and complete *without* a cycle-collector backstop. They
are not new — AILang already satisfies all four — but the
[memory model](0008-memory-model.md) makes them load-bearing rather
than incidental:

1. **Strict evaluation.** Every `Term::App` (see
   [Data model](0002-data-model.md)) argument is fully
   evaluated before the call. No laziness, no thunks. (Already
   true.)
2. **No recursive value bindings.** `(let x EXPR ...)` evaluates
   `EXPR` in a scope where `x` is *not* bound. Recursion is
   exclusively via `Term::LetRec` (which binds a fn, not a value)
   and module-level fn defs. (Already true.)
3. **No shared mutable refs.** Values are immutable once
   constructed. There is no `ref`, `IORef`, `Mutex`, or any
   primitive that allows a value to be mutated from a position
   outside its allocation. (Already true.)
4. **ADTs are acyclic by construction.** Strict evaluation +
   no-recursive-value-bindings + no-shared-mutable-refs together
   guarantee that any value graph reachable from a binding is a
   DAG. The reference graph has no cycles. (Follows from 1–3.)

Laziness, recursive value bindings, shared mutable state, or any
feature that creates cycles is rejected at design time unless the
proposal proves the cycle is collectible by an extension (e.g.
linear ownership).

These constraints are the precondition for the
[memory model](0008-memory-model.md): a sound RC implementation without
a cycle-collector backstop requires the reference graph to be a
DAG, which constraint 4 establishes from 1–3. They are also the
load-bearing structural reason behind several rejections under the
[feature-acceptance](0004-feature-acceptance.md) bug-class-reintroduction
discriminator (notably iterated-mutable-state reasoning).

Ratified by: `crates/ailang-check/src/uniqueness.rs` (in-source mod tests).
