# 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. The
[memory model](0008-memory-model.md) relies on all four:

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).

Guaranteed by construction, not by a positive test: the AST has no
thunk, `ref`, or `IORef` node, and `(let x EXPR ...)` binds `x` only
in the body, never in `EXPR` — there is no construct that could
violate constraints 1–3, and constraint 4 follows from them. The
binding force is the design-time
[feature-acceptance](0004-feature-acceptance.md) gate, which rejects
any proposal that would reintroduce one of them.