Developers / Memory management

Memory management

Moth is reference-semantic by default, copy-explicit and move-inferred. It omits explicit reference types and lifetime syntax, not references themselves.

Moth keeps the source model small. Reads are shared, copies are explicit and mutation has to announce itself.

Memory safety comes from static proof, not from a collector. Borrow validation enforces exclusive mutation and last-use safety. Lifetime-topology validation enforces one lifetime owner per allocation family and legal retained edges. Both run under every backend and every build profile.

Garbage collection is a permitted representation of a topology that is already proven legal. It is not the correctness baseline, and release builds on backends that advertise full memory control lower every accepted program without a tracing collector.

Shared access vs copy

Existing values use shared, read-only access by default. Binding a new name to an existing value doesn't copy it. Use copy when you need an independent value.

Shared aliases use last-potential-use activity, not pure lexical lifetime. After the final potential use of a shared alias, later mutation may proceed.

items ~= {"a", "b"}
shared_items = items

change(~items)       -- invalid: shared_items is used again
inspect(shared_items)

items ~= {"a", "b"}
shared_items = items
inspect(shared_items)

change(~items)       -- valid: shared_items has no later potential use

items ~= {"a", "b"}
copied_items = copy items

change(~items)
inspect(copied_items)

Exclusive access

~place requests temporary mutation-capable access to an existing mutable place. It isn't a move marker or a type identity. Fresh rvalues satisfy ordinary mutable parameters without source ~. Mutable receivers still require an existing mutable place.

change({"fresh"})

Lifetime owners

Every runtime allocation family has exactly one semantic lifetime owner. Multiple bindings or fields may alias that allocation without becoming additional owners.

An object may retain a reference only when the referenced allocation belongs to the same lifetime region or to a region statically known to outlive the retaining object.

Inferred regions are compiler-generated intervals over control flow, not plain lexical scopes. The compiler starts from the narrowest valid owner and widens only along the nearest enclosing ancestor. It never promotes across independently ending siblings and never invents a page or application owner to avoid a diagnostic.

The compiler rejects illegal sibling sharing and cross-region cycles on every backend. GC is a permitted representation for a statically legal topology, not a way to accept invalid retained edges.

Declared name: / into name syntax is accepted end-state design with implementation deferred. It is the only source mechanism for reference cycles. See Declared regions for the source contract and Lifetime regions and escape validation for the general topology model.

How the compiler layers it

source access, copy and declared-region syntax
    -> AST access-mode, placement and freshness validation
    -> validated HIR with explicit places and control flow
    -> borrow and last-use analysis
    -> local allocation-family and retained-edge constraints
    -> project and package summary instantiation
    -> complete backend-neutral lifetime-topology validation
    -> non-lexical interval, frontier and epoch completion
    -> backend-neutral memory requirements
    -> target-affinity analysis and partition
    -> target-contract validation
    -> per-physical-variant family/layout refinement
    -> target/profile-aware compiler-owned memory planning
    -> ValidatedMemoryPlan validation
    -> backend memory lowering

Detailed pages

• Access and aliasing: shared reads, explicit copies and ~ access
• Borrow validation: roots, joins, last-use facts and affine transfer safety
• Boracle: the developer-facing reference borrow model, its borrow-analysis laboratory and the bounded operational oracle it is compared against
• Checked proof-budget research: future opt-in deep analysis that trades compile time for proof precision without changing safety rules
• Lifetime regions and escape validation: one owner, retained edges, non-lexical intervals, cleanup frontiers and escapes
• Declared regions: accepted deferred name: / into name semantics and hard bulk lifetimes
• Retained Edge Counting: the narrow counted strategy for runtime-many persistent retained edges
• Affine ownership and drops: affine cleanup responsibility, the ownership ABI and conditional destruction
• Runtime and backend lowering: physical strategies and the collector-free release guarantee

Current support

See Progress matrix for what is implemented today. Most of this model is accepted design with implementation deferred. Checked proof-budget scopes remain an open proposal and are intentionally absent from the progress matrix.