Documentation / Design scope

Design scope

Moth distinguishes three outcomes for a proposed feature. Accepted deferred work belongs to the language design but still awaits implementation. Open design questions have no accepted contract yet. Features outside scope conflict with the language design.

These distinctions prevent an unsupported feature from looking like a design promise, and they explain why Moth chooses constrained templates, choices and static traits over broader mechanisms found in other languages.

Design principles

Moth is a small language by design. Every feature has to earn its place.

How Moth decides

The language prefers one clear mechanism over many specialised syntax forms. When a problem can be solved with an existing feature, the language doesn't add a second way to do it.

-- Templates handle text composition
greeting = [: Hello, [name]]

-- Choices handle runtime heterogeneity
Status :: Ready, Waiting | reason String |;

-- Error! handles expected failures
result = parse(text)!

What this means for you

  • fewer syntax forms to learn
  • code from different authors looks similar
  • the compiler can give clear error messages
  • behaviour stays explicit instead of relying on hidden magic
  • the language keeps a small surface area
  • the compiler can resolve code statically
  • optimisations happen behind the scenes

Source stays platform-agnostic

Authors write against Moth and builder-provided capabilities. The builder decides how those semantics become JavaScript, Wasm or another artefact; source does not test which target was selected. Build configuration is not target detection.

Moth keeps the source language small. Compiler complexity is acceptable when it makes the programmer-facing model simpler, safer and more predictable. Keep source behaviour statically resolved and locally inspectable. Hide backend optimisation behind stable semantics so implementation techniques do not become source-language obligations.

Central bias

  • keep the source language small, explicit and statically inspectable
  • prefer constrained built-in mechanisms over general metaprogramming
  • prefer static resolution over runtime dynamism
  • keep backend optimisations hidden behind stable source semantics
  • avoid features that need pervasive solver-heavy reasoning

Preferred constrained mechanisms

Need

Preferred mechanism

Compile-time generation

Templates, constants and builder directives

Static reuse

Generic functions and explicit trait bounds

Runtime heterogeneity

Choices

Expected failure

Error!, postfix propagation and catch

Invariant failure

assert

Explicit result-like domain values

Ordinary choices

Platform integration

Builder packages, external packages and source-backed packages expose stable capability semantics. Project builders and backends resolve those semantics to platform-specific artefacts.

Memory safety

Mandatory borrow validation plus mandatory lifetime-topology validation. Static proof is the baseline; a garbage-collected representation is one permitted physical representation, never the correctness mechanism.

Mutation

Explicit exclusive access rather than implicit mutation

Ownership

Compiler-inferred affine cleanup transfer rather than source-visible move or lifetime syntax

Release memory

Backends that advertise full memory control lower release builds without a tracing collector. This is a backend capability, not a source or project mode.

Declared bulk lifetimes

Accepted deferred name: / into name hard lifetime regions

Performance

Hidden compiler and backend optimisation

Platform-agnostic source and builder ownership

Source expresses stable semantics rather than target identity. Source cannot inspect the OS, architecture, backend or target, and cannot condition imports, declarations, exports or bodies on target identity. Implemented #Config values provide typed project/build configuration, and explicit @project provides immutable project fields; neither is platform detection. Entry-local config: blocks remain deferred.

Builders cannot expose target identity as pseudo-config values. A selected builder may expose stable capability APIs, and compiler target validation rejects unsupported reachable capability use. Project builders own target partition and output form, the compiler-owned memory planner owns physical memory strategy per target/profile variant, and backends realise those decisions. This boundary is intentional outside-scope policy, not merely deferred syntax.

Design review questions

  • Does this introduce a new source category when an existing mechanism is enough?
  • Does it make behaviour more implicit?
  • Does it need whole-program or solver-heavy reasoning?
  • Does it introduce erased runtime machinery?
  • Does it leak backend representation?
  • Does it expose optimisation mechanics?
  • Is it accepted but unimplemented, undecided or intentionally excluded?
  • Does it make code harder to inspect locally?
  • Does this let source observe or branch on a physical target, backend or runtime platform that should remain builder-owned?

LLM-aware design

Coding agents are increasingly becoming a part of coding workflows.

Moth is designed to be strict and provide clear and fast feedback to coding agents.

Developers can focus more on high level design, architecture or important implementation detailed, while agents handle the busy work.

Good languages for the future should be easy to review and strict about what the code should look like and how it's structured. This means developers can worry less about whether their code is reliable / memory safe / structured correctly / using the correct patterns or idioms.

A small syntax, strict rules, opinionated design, fast tooling and good diagnostics give agents less space to make mistakes or drift from ideomatic code.

Compiler diagnostics should carry stable codes, structured facts and source metadata for editors, development servers and coding agents.

Moth has very little training data, but this may be useful later: examples can grow around the language that exists and agents will have to follow your codebase style more strictly. No legacy patterns to pollute generated output.

See HUMANS.md for more general stances and opinions on getting good output out of LLMs.

Read next

Deferred, open and outside scope

Moth has three ways to describe a feature that isn't available today.

Accepted but not built yet

Some features belong to the accepted design but aren't built yet. Examples include declared regions and recursive choice types. These features may appear in the progress matrix as implementation work.

Still being considered

Some ideas have no final contract. Moth may consider distinct primitive-backed nominal wrappers, narrow named function references and checked proof-budget blocks.

A checked proof-budget block would let the compiler spend much more time trying to prove difficult code safe. Code outside the block would still receive the same mandatory safety checks. The working name and syntax are not accepted yet.

Not part of Moth's design

Some features conflict with Moth's design goals. The compiler rejects them, and the error message won't say "coming soon" because they aren't accepted work.

Target-, OS-, architecture- and backend-specific source is outside scope, not deferred; builders own platform mapping.

Why exclude features?

Moth prefers:

  • one clear mechanism over many specialised forms
  • static resolution over runtime dynamism
  • explicit behaviour over implicit magic
  • small surface area over broad feature coverage

When a feature would make the language broader, more implicit or harder to reason about locally, Moth says no.

Moth separates future work and exclusions into three categories.

Deferred, open and outside scope

The progress matrix tracks implementation of accepted design. It intentionally omits open design questions and outside-scope features.

Accepted deferred implementation

The semantic or architectural contract for a deferred feature fits Moth's language design. Implementation may be absent, partial or target-limited. A deferred feature may appear in the progress matrix and may have a structured deferred-feature diagnostic. A roadmap plan owns sequencing, not semantics.

Examples of deferred features:

  • declared regions (name: / into name)
  • mandatory lifetime-region and escape validation
  • choice payload field access without pattern matching
  • nested choice payload patterns
  • recursive choice types
  • generic external package functions and types
  • package manager, versions and lockfiles
  • broader standard trait taxonomy
  • field/path reactive subscriptions
  • first-class filesystem path values, directory values and runtime filesystem access
  • source-file reflection and reading .moth source as text
  • constructing a file reference from a runtime String
  • an extensionless resource escape syntax
  • managed plain Markdown resource links and images
  • resource transforms and content-addressed output names

Open design question

An open design question has no final accepted contract. It may or may not enter the language. It isn't a promise and must not appear in the progress matrix. A roadmap document or discussion doesn't make it accepted design, and the compiler needn't provide a "coming later" diagnostic.

Current open questions include:

  • distinct primitive-backed nominal wrapper or newtype syntax
  • narrow references to named, monomorphic, non-capturing functions
  • checked proof-budget blocks, an opt-in lexical scope that may permit much deeper static analysis in exchange for substantially slower compilation

The checked-block name and example spelling are only working proposal language. The safety rules, source meaning and runtime behaviour would remain the same inside and outside the scope.

Transparent aliases remain transparent regardless of whether a distinct primitive-backed nominal wrapper enters the language.

Outside scope

An outside-scope mechanism conflicts with the intended language model and needs an explicit design-philosophy change before implementation. The exhaustive excluded-family inventory below records these mechanisms. They don't appear in the progress matrix.

The compiler rejects outside-scope forms with ordinary diagnostics.

Target, OS, architecture and backend conditional source is outside scope rather than deferred. Builders own platform mapping.

Outside-scope features aren't "not yet implemented." They're intentionally excluded because they would make the language broader, more implicit, more solver-heavy or harder to reason about.

See Excluded language families for the exact list.

How to tell the difference

Ask whether Moth already has an accepted contract for the feature. If it does and implementation remains absent, partial or target-limited, the feature is deferred. If the mechanism conflicts with Moth's language model, it stays outside scope. A proposal with neither an accepted contract nor a conflict with that model remains an open design question.

Diagnostic distinction

A deferred-feature diagnostic tells the author that accepted syntax hasn't landed yet. An outside-design-scope diagnostic tells the author that the form conflicts with the language model and won't be accepted without an explicit design change.

Both use structured CompilerDiagnostic. The distinction matters because the remedy differs: a deferred feature needs implementation progress, while an outside-scope form needs a different approach or a language philosophy change.

The progress matrix at Progress matrix reports whether a deferred surface is implemented today. This page explains whether the surface belongs in the language at all.

Read next

Future proposal: checked proof-budget blocks

This is an open proposal. The name and syntax are not accepted yet.

What it would do

A checked proof-budget block would let the compiler spend much more time trying to prove difficult code safe:

checked:
    -- code that needs unusually deep analysis
;

The compiler would still run its normal fast analysis first. It would only use the expensive tier when the normal checker found a possible conflict it could not settle.

What it would not do

Code outside the block would still receive every mandatory safety check. A checked block would not:

  • change runtime behaviour
  • weaken borrow or lifetime rules
  • make garbage collection a safety fallback
  • accept code because testing found no failure
  • let source choose a solver or time limit

It would trade compile time for proof precision, not safety for convenience.

Predictable limits

The deeper checker would use deterministic limits such as a maximum number of states or refinement rounds. It would not try for a machine-dependent number of seconds.

If the compiler reached its limit, the code would remain unproven. The compiler would never treat "no counterexample found yet" as proof.

Why it may help

The deeper tier could keep more branch relationships separate, reason more carefully about loop generations, specialise call summaries or prove that two indexes cannot refer to the same element.

Boracle will research these proof techniques before Moth decides whether a source feature is worthwhile. The proposal should become accepted design only if the deeper tier proves a useful class of safe programs that the normal checker deliberately rejects for compile-time cost reasons.

This is an open design proposal. It is not accepted syntax, a progress-matrix feature or an implementation promise.

Core idea

Moth's normal compiler should use a predictable, efficient borrow analysis that proves common programs without turning every build into symbolic execution. Some safe programs still need substantially more path, value or loop reasoning than the normal checker should spend by default.

The proposal introduces a lexical proof-budget scope. The working name is a checked block:

checked:
    -- difficult but safe alias relationships
;

The example spelling is illustrative only. The final keyword, placement rules and exact scope shape remain open.

A checked scope would let the compiler spend much more compile time proving the same static safety rules. It would not make code outside the scope less checked.

Same rules, different analysis effort

The proposed meaning is:

ordinary source
    -> normal proof budget

checked scope
    -> normal proof budget first
    -> deeper proof only when the normal analysis cannot decide

The safety contract would remain identical:

  • shared and exclusive accesses still cannot conflict
  • copies still create independent values only through copy
  • optional ownership transfer still requires a complete final-use proof
  • lifetime topology still needs one legal owner and valid retained edges
  • garbage collection still cannot make invalid source legal
  • backend choice still cannot change accepted source

A checked block would affect compiler effort, not runtime meaning.

Candidate analysis ladder

The future production checker is expected to start with cheap analysis and only refine a candidate conflict when needed. Checked scopes fit that structure:

cheap borrow solve
    |
    +-- proven safe -> accept
    |
    v
candidate conflict
    |
    v
normal conflict-directed refinement
    |
    +-- conflict disproved -> accept
    |
    v
checked proof scope?
    |
    +-- no -> report the remaining conflict
    |
    v
deep refinement
    |
    +-- conflict impossible -> accept
    +-- conflict possible -> report one compatible witness
    +-- proof limit reached -> report that proof remained inconclusive

The normal path should still handle most code. The checked tier exists for analyses whose cost would be unreasonable as the default.

Possible deep analyses include:

  • retaining many more branch-correlated state alternatives
  • delaying conservative widening at control-flow joins
  • stronger loop-generation and induction reasoning
  • richer outcome-sensitive call-summary instantiation
  • value-sensitive fixed-index or inequality proofs
  • larger conflict slices and more complete witness reconstruction
  • later investigation of narrow solver-backed path-feasibility queries

None of these techniques is accepted merely because this proposal names them. Each still needs an independent soundness review.

Analysis enclave

A checked scope should not become an isolated mini-function. Values, aliases and capabilities may enter the scope and later uses may occur after it.

A likely architecture is:

normal entry facts
    -> checked deep refinement
    -> compact proven exit facts
    -> normal analysis continues

The compiler may inspect predecessor provenance and later uses outside the lexical block when the proof requires them. The scope authorises expensive state splitting and refinement around obligations caused by the scope. It should not silently turn the whole module into deep symbolic execution.

Useful exit facts may include:

  • two origins must be disjoint
  • two places must observe the same generation
  • a loan cannot reach one exit
  • a result has one of several path-correlated provenance shapes
  • a value has no future use on a specific continuation

The ordinary checker can consume those compact facts without retaining the full deep state outside the scope.

Deterministic compile-time budgets

The compiler must not decide legality by trying for a wall-clock duration such as five seconds. Machine speed, system load and cache state must not change whether a program compiles.

A checked analysis needs deterministic semantic limits, such as:

  • maximum refined states
  • maximum path alternatives
  • maximum loop-refinement rounds
  • maximum tracked predicates
  • maximum specialised summary obligations
  • maximum solver obligations if a solver is ever introduced

The exact limits are compiler implementation policy. Source should not select a numeric budget or a solver algorithm.

Reaching the hard limit means the compiler could not prove the program within the supported checked tier. It never means "probably safe".

Monotonicity

A useful final design should preserve these properties:

normal analysis accepts P
    -> checked analysis also accepts P

checked analysis accepts P
    -> the same ordinary Moth safety rules are proven

removing checked
    -> may lose a difficult proof
    -> never changes runtime meaning

Adding checked must not activate a stricter source law or produce a different runtime operation. It only permits more analysis.

Relationship to Boracle

Boracle is the right place to research the proof techniques before source syntax is accepted.

The research sequence should distinguish:

coarse result
normal refinement result
deep refinement result
proof effort required

A case is useful evidence for this proposal when:

  • normal analysis reaches a deliberate precision or cost boundary
  • a deeper deterministic analysis proves the case safe
  • the proof has a path-compatible explanation
  • independent operational testing finds no bounded counterexample
  • the deeper rule has a written static soundness argument

Boracle's bounded operational oracle remains a counterexample finder and test oracle. A finite set of successful executions can never replace the static proof required for checked acceptance.

Possible future use beyond borrow conflicts

Borrow precision is the primary motivation. The same proof-budget marker could later inform other static analyses when their own contracts support a deeper tier:

  • last-use and optional-transfer precision
  • lifetime-region and escape proofs
  • cleanup-frontier and retained-edge reasoning
  • proving that REC is unnecessary in a difficult case
  • bounds-check or checked-arithmetic elimination

These consumers must remain separate analyses. A checked block must not merge borrow legality, lifetime topology and physical memory planning into one solver.

Hard constraints for any accepted design

  • Normal Moth remains fully statically checked.
  • Checked code uses the same safety and runtime semantics as ordinary code.
  • Cheap analysis runs before deep analysis.
  • Deep analysis is conflict-directed rather than unconditional whole-module work.
  • Compile-time limits are deterministic and semantic, not wall-clock timeouts.
  • Exhausting the proof budget cannot accept code.
  • The backend sees no runtime checked-block operation.
  • Source cannot choose a solver implementation or numeric budget.
  • Cross-module calls continue to use stable semantic summaries.
  • A checked caller does not open arbitrary dependency HIR as local control flow.
  • Bounded operational execution is evidence, not acceptance proof.
  • The proposal does not make Boracle a user-selectable compiler fallback.

Open questions

The design remains open on:

  • whether checked is the right name
  • whether the feature should be block-only or also allow a whole function
  • how nested checked scopes compose
  • which deep proof families are worth supporting first
  • how the compiler reports a true conflict versus exhausted proof effort
  • which compact exit facts may escape the scope
  • whether lifetime analysis should reuse the same marker later
  • whether narrow path-feasibility solving is worthwhile after custom Moth-specific domains
  • what deterministic hard limits provide useful power without pathological builds

The syntax should remain unaccepted until Boracle demonstrates a meaningful set of safe programs that need the deeper tier and the compiler can explain those proofs clearly.

Why the proposal may fit Moth

Moth deliberately removes many features that make general borrow checking hard: there are no source-visible lifetime parameters, general closures, function values, trait objects, raw pointers or unsafe escape hatches. Calls are static, generics are concrete before borrow validation and builtin storage effects are compiler-known.

Those restrictions make an unusually strong deep static tier plausible. The proposal uses that advantage without forcing every ordinary build to pay its worst-case cost.

Excluded language families

Moth says no to many features that other languages include. Here is why.

No general macros

Macros create a second language inside your code. Moth uses templates, constants and builder directives for compile-time work instead.

No general closures or higher-order function values

General closures and higher-order function values add complexity to the type system and make code harder to follow. Moth uses reactivity for the common UI pattern that closures usually solve.

No dynamic trait values

Dynamic trait values need runtime dispatch and hidden wrappers. Moth uses choices for runtime variety and generic bounds for static reuse.

No operator overloading

Operators in Moth always do the same thing. You can't redefine + or == for your own types.

No reflection

You can't inspect types at runtime or write code that examines other code's structure. This keeps programs predictable and easy to read.

No platform-specific source branches

Moth code does not ask whether it is compiling for an operating system, architecture, JavaScript or Wasm. Builders handle that choice.

No explicit lifetime and ownership type system

Moth keeps lifetime and ownership rules behind the compiler. Source code uses explicit copies and exclusive access without adding lifetime or ownership annotations.

No general blocks or control-flow labels

Structured control flow introduces scope. Moth has no dedicated general lexical-block construct, statement labels, labelled loop exits or goto. block is an ordinary identifier, so block: declares a region like any other valid name: header. Exact _: is invalid.

The pattern

Each excluded feature has a Moth replacement that is more constrained and more explicit. The language trades generality for clarity.

This file forms the exhaustive inventory of language mechanisms outside Moth's design scope. A listed feature needs an explicit change to the language philosophy before implementation.

Macros and broad metaprogramming

General-purpose macros, procedural macros, derive macros and AST macros create a second compile-time language and make code harder to inspect. Templates, constants and builder directives provide the constrained compile-time surface.

General closures and broad function-value mechanisms

General closures, anonymous callable values, generic function values and higher-order polymorphism are outside scope. These mechanisms add broad function-value semantics and solver pressure. Reactivity covers many closure-heavy template cases without adding general function values. Hidden event-handler closures remain outside the language model as well.

Dynamic trait values

Dynamic trait values and trait objects require erased wrappers, runtime dispatch, dynamic-safety rules, backend-specific runtime support and a second meaning for trait names. Use choices for runtime heterogeneity and generic trait bounds for static reuse.

Trait-level programming

Trait inheritance, trait aliases, trait composition, default methods, associated types and associated constants turn traits into a type-level programming system rather than simple method contracts.

Generic traits and generic trait methods

Generic traits and generic trait methods make trait solving significantly more complex and create Rust-like abstraction patterns.

Conformance extensions

Blanket, conditional, negative, specialised and structural conformance require coherence and specialisation rules outside Moth's simplicity target. Structural conformance must not silently imply conformance from matching method shapes. Type must TRAIT stays explicit. File-local evidence-backed bound dispatch outside reusable conformance, output coercion, operator integration, automatic primitive conformance and derive-style hashing, ordering, formatting, iteration or serialisation families also stay outside scope.

Constraint sublanguage

Type-set constraints, union constraints, underlying-type constraints and user-defined numeric or operator constraints turn generic bounds into a constraint sublanguage. Generic bounds name traits only. where clauses remain outside the source constraint model.

Operator overloading

Operators stay compiler-owned and predictable. Moth has no source-visible operator overloading.

Source-authored receiver extensions

Cross-file, builtin, imported and foreign receiver extensions remain outside scope. Source-authored receiver methods belong only to the same file as their nominal receiver type. Methods for dependency package types and external opaque types must use free functions.

User-extensible map semantics

User-defined HASHABLE, custom map hashers or comparers and user-defined keys for builtin maps stay outside the language. Builtin map syntax stays scalar-keyed. More sophisticated maps belong in packages as ordinary structs.

Builtin keys remain limited to String, Int, Bool and Char. The builtin map surface excludes Float, structs, choices, collections, maps, traits, functions, external opaque types and generic parameters as key families. It also excludes hashset syntax, map equality, indexing syntax, mutable entry APIs, const maps, fixed-capacity maps and specialised map variants.

First-class result values

First-class public Result values and result pattern matching stay outside the language. Error!, postfix ! and catch form the error path. Authors can define ordinary choices when they want explicit result-like domain values.

User-defined cast extensions

User-defined cast target types, generic cast target parameters, external opaque cast targets, generic cast traits, broad return-type-directed conversion and implicit conversion chosen from distant context remain outside scope. Cast evidence stays compiler-owned and explicit.

Exceptions and catchable panic systems

Expected failures use Error!. Invariants use assert. Moth has no public exception or catchable panic system. The two lanes stay distinct: Error! handles recoverable failure and assert handles impossible invariant violation.

Reflection and type introspection

Reflection, type values, runtime type IDs, compile-time type inspection and type-returning functions encourage generic metaprogramming and weaken static readability.

Higher-kinded types

Higher-kinded types, type functions, partial application and parameterized type aliases introduce a type-level abstraction language.

User const generics

User const generics beyond fixed collection capacity stay outside the language. Capacity syntax remains a small built-in collection feature, not a general type parameter system.

Source-visible memory annotation systems

Source-visible lifetime, reference-category and ownership annotation systems stay outside the language. Moth omits explicit reference types and lifetime syntax, not references themselves. The compiler tracks ownership and lifetimes internally. Source-visible lifetime parameters, temporary-reference syntax, explicit move syntax and separate borrowed and owned function signatures remain outside scope.

General lexical blocks and control-flow labels

Moth has no dedicated general lexical-block construct. block is an ordinary identifier, so block: has the same declared-region meaning as any other valid name: header. Anonymous _: blocks and brace replacements remain outside scope. Structured control flow introduces ordinary lexical scopes, while bare identifier: headers belong exclusively to declared regions.

Arbitrary statement labels, labelled break, labelled continue and goto remain outside scope. Unlabelled loop exits stay structural and target the nearest enclosing loop. Keyword-led semantic scopes such as async: remain distinct because their keyword carries language-defined behaviour.

Source-visible RC and dynamic shared ownership

Source-visible RC, retain/release, weak ownership, finalisers and unrestricted dynamic shared ownership stay outside the language. Diagnostics, common declared regions, copy and builder lifecycle roots replace source-level RC.

Retained Edge Counting is a compiler-selected physical representation for already-legal topology. It is not source syntax, not a type, and no program can name, observe or request a counter. There is no source REC.

Inferred cyclic regions

The compiler never invents a cyclic lifetime region to accept a program. Direct source-created reference cycles are legal only inside one declared region, where storage is count-free and reclaimed in bulk at declared-region exit. Cross-region cycles are invalid, and Moth has no cycle collector.

Backend-specific source legality

No backend or build profile may change which source programs are valid. Borrow validation and lifetime-topology validation run identically everywhere, and debug, GC-native and collector-free paths accept and reject exactly the same source with the same observable behaviour. There is no source-visible or project-visible no-GC mode.

Target-conditional source and backend-specific semantics

Moth excludes target, OS, architecture and backend identity from source semantics. In particular, the language has no:

  • target_os, target_arch, backend-name or target-name source queries
  • is_wasm, is_javascript or is_browser style build flags
  • target-conditioned imports
  • target-conditioned declarations and exports
  • target-conditioned receiver methods, traits or conformances
  • backend-dependent language legality or observable semantics
  • use of #Config to recreate these mechanisms

The replacement is builder capability surfaces, target-contract validation, external/builder packages, and backend-owned lowering and artefact policy. Source can use a stable capability API without learning which backend implements it. Backends receive validated topology and may not reconsider source legality.

Read next