One semantic model, carried all the way through.

Stable identities

Canonical source, module, and definition IDs drive diagnostics, caching, module cycles, navigation, and coherence checks.

Explicit MIR operands

Local reads are not ambiguous: MIR records whether an operand copies or moves, including projected places and partial moves.

One tooling truth

check, typeof, hover, completion, navigation, references, formatting, and verification reuse compiler facts instead of parallel heuristics.

Generated language artifacts

A structured grammar model produces EBNF, JSON grammar, keywords, editor metadata, and formatter spellings with a drift gate.

Parameter modes expose transfer

f consume(items: Vec[Item])
f inspect(ref items: Vec[Item])
f update(ref mut items: Vec[Item])

Owned non-Copy values move. Shared references read; mutable references are exclusive. mv can document a move but is not required for an owned transfer.

Second-class, provenance-checked references

References cannot be stored in ordinary aggregates, captured by escaping closures, or sent to tasks. A returned reference is allowed only when derived from a reference parameter under elision rules.

Compiler-known ownership traits

Copy, Clone, Drop, Send, and Sync have structural validation. Types with Drop are never Copy; duplication of affine values uses explicit clone(value).

Exactly-once destruction

CFG and overwrite drop elaboration destroy each owned place once. Partial moves drop only initialized fields. The initial panic strategy is abort; compiler-generated cleanup covers abort and contract paths.

Call-graph effect inference

Effects flow through direct calls. Compiler results can explain why a function requires file, network, process, environment, or unsafe authority.

Registry-driven enforcement

Builtins declare signature, ownership policy, effects, and capability requirements centrally so checking, runtime denial, and documentation cannot drift independently.

Normal file I/O remains possible

Capabilities are not a ban on useful programs. --allow-read and --allow-write grant file authority; other authority remains denied unless granted.

Defense in depth remains optional

Interpreter containment, limits, denial, and solver process cleanup ship in 0.2. OS process isolation is an additional option for untrusted playgrounds, verification, build scripts, or third-party code.

One file, one module

Imports resolve relative to the importer or package root. pub controls visibility, explicit exports bind deterministically, and cycles receive stable diagnostics.

Coherence without source-order luck

Overlapping implementations and specialization are initially disallowed. Inherent methods win, then imported traits, then prelude traits; unresolved ambiguity is an error.

Manifests and lockfiles

forma.toml and generated forma.lock support deterministic local path dependencies now. Registry and Git sources are rejected rather than guessed.

Semantic LSP foundation

Diagnostics, hover, completion data, symbols, navigation, references, signatures, and formatting share compiler state. Richer member ranking and refactoring remain evolution work.

Generated testing

forma verify rules.forma \
  --level test --examples 200 --seed 42

Reproducible generated inputs run under step and time limits. Passing samples produce TESTED, never PROVED.

Finite exhaustion

forma verify rules.forma \
  --level exhaustive --max-domain 4096

Supported finite parameter domains are enumerated completely. Reports state the tested domain and return UNKNOWN if it is unsupported or too large.

Formal attempt · Experimental

forma verify rules.forma \
  --level formal --report

The SMT backend covers acyclic signed-64-bit Int/Bool logic plus structural tuples and named structs made from those leaves. It proves construction, projection, equality, projected updates, and struct-invariant establishment/preservation; unsupported or timed-out work remains UNKNOWN.

Human and machine explanations

forma explain rules.forma --format human
forma explain rules.forma --format json

Contracts can be explained for reviewers or automation without creating a second interpretation of their meaning.