1. Introduction & Design Philosophy

Generated from 01-introduction.md. Handbook SHA-256: a5d21aff583bfbb6d9db8ef52b842fec80adad1864f5846488ab5bc00e090e24

Ultraviolet is a general-purpose systems programming language. Per the Language Design Contract (§0.4 of the specification), it is “a general-purpose systems programming language optimized for source code written by humans, generated by AI systems, and reviewed by humans.” This single sentence is the most important framing in the entire language: every other rule in the specification exists to make code that is unambiguous to write, mechanical to generate correctly, and fast to verify by reading. This chapter establishes what Ultraviolet is for, the four foundational design rules and their concrete consequences for everyday code, the exact text of the Language Design Contract, how the specification and this handbook are organized, the overall mental model a developer must hold, and how the philosophy shapes API and module design.

This is a reference chapter: it sets the vocabulary and the rules of engagement. The concrete syntax for each construct mentioned here is owned by a later chapter, and this chapter cross-references those chapters by name. Where this chapter shows a code example, the example is valid per the specification, but the construct’s full grammar, parsing, static semantics, dynamic semantics, lowering, and diagnostics live in its owning chapter.

Note on the section number. The Language Design Contract is §0.4, inside Chapter 0 (Front Matter). In the specification, §1.4 is “Normative References,” not the contract. This handbook cites the contract as §0.4 throughout.

1.1 What Ultraviolet Is

Ultraviolet is a statically compiled, systems-level language. It targets native code through an LLVM 21 backend; LLVM 21 is the single normative backend (§1.4 Normative References, reference [LLVM21]; backend requirements live in “Common Lowering, Program Lifecycle, and Backend”). It is built for programs where the author must reason precisely about memory, ownership, responsibility, authority, synchronization, suspension, and lifecycle — engines, runtimes, tooling, simulations, and other software where correctness and control matter more than convenience shorthand.

Three audiences are first-class, and the language is shaped by all three:

• Humans writing code. The surface syntax is designed so that a single correct spelling exists for each operation; the author never has to choose between equivalent forms.
• AI systems generating code. A language with exactly one accepted form per operation is far easier to generate correctly, because there is no ambiguity to resolve and no stylistic dialect to pick. The handbook you are reading exists precisely so that human and AI authors share one authoritative description of correct, compiling Ultraviolet.
• Humans reviewing code. Authority, mutability, ownership, copy/move/reference behavior, synchronization, suspension, and dynamic-check behavior must all be visible from local syntax. A reviewer should never have to chase a definition across the codebase to know whether a line allocates, copies, moves, blocks, suspends, or acquires authority.

These three audiences are not a marketing list. They are the justification used throughout the specification to accept or reject design choices, and they are the reason the four foundational rules below are non-negotiable.

What “general-purpose” and “systems” mean here

“General-purpose” means Ultraviolet is not restricted to a single domain; it provides the full apparatus of a modern typed language — records, enums, classes, modal types, polymorphism, contracts and invariants, structured parallelism, async, compile-time execution and metaprogramming, and a foreign-function interface. “Systems” means the language exposes and demands precision about the machine-level and resource-level facts that higher-level languages hide: where memory lives, who owns it, when it is freed, what runs concurrently, where the program suspends, and where it crosses a trust boundary into foreign code. The design rules in §1.2 are how Ultraviolet keeps that precision legible instead of letting it sink into invisible defaults.

1.2 The Four Foundational Design Rules

The Language Design Contract (§0.4) states four principles. A conforming design change SHOULD preserve all four. For a developer, they are not abstract goals — each one produces concrete obligations and concrete prohibitions that you will feel on every line you write. The four rules are: One Correct Way, Local Reasoning, Explicit over Implicit, and Static by Default.

1.2.1 One Correct Way

The first principle, verbatim from §0.4:

1. One Correct Way.
   Where possible, each semantic operation in Ultraviolet MUST have exactly one accepted source form.

   A language feature SHOULD NOT introduce aliases, shorthand forms, optional equivalent spellings, or syntactic sugar that lower to the same AST form and have identical static and dynamic semantics.

   An alternate source form is permitted only when it changes at least one of:

   1. static semantics;
   2. dynamic semantics;
   3. authority or capability requirements;
   4. ownership, movement, copying, or responsibility;
   5. synchronization behavior;
   6. suspension behavior;
   7. ABI, layout, or foreign-boundary behavior;
   8. diagnostic behavior in a way that is part of the language contract.

   Formatting whitespace and comments are not semantic source forms for this principle, but grammar-level alternatives are.

Semantics. There is exactly one accepted spelling for each operation. Two spellings are allowed to coexist only when they differ in at least one of the eight enumerated dimensions — that is, only when they actually mean something different. If two forms would lower to the same AST and behave identically statically and dynamically, the language does not provide both. This is why Ultraviolet has no “convenience” aliases, no optional sugar that desugars to a longer form, and no two-ways-to-write-the-same-thing.

Concrete consequences for everyday code:

• There is no choice paralysis. When you need to move a value, there is one form. When you need a local binding, there is one binding statement form. You do not pick between equivalent spellings.
• A diff is meaningful. Because there is no cosmetic spelling variation, a change in the source almost always reflects a change in meaning. Reviewers do not waste attention on “they rewrote this the other way.”
• Generated code is canonical. An AI generator does not have to learn a house dialect; the language is the dialect.

Note carefully the last sentence of the principle: grammar-level alternatives are semantic source forms. Whitespace and comments are free, but a second grammar production that produces the same AST is exactly what One Correct Way forbids. The rule is therefore enforced at the grammar level, not merely as a style suggestion.

The let versus var distinction is the canonical illustration that One Correct Way is about meaning, not about minimizing keywords. Both introduce a local binding, but they parse to different AST forms — LetStmt and VarStmt — because they are different operations: let introduces an immutable binding, var a reassignable one. They are not aliases; they are two operations distinguished under dimension 4 (ownership, movement, copying, responsibility).

A second, subtler example lives inside the binding statement itself. The binding operator is binding_op ::= "=" | ":=", and the two forms differ semantically: = is a move-initializer (MovOf("=") = mov) and := is an immovable initializer (MovOf(":=") = immov). They are not interchangeable sugar; they encode different movement behavior (again dimension 4), so both are permitted to exist. The everyday form is =.

procedure summarize(values: [i32]) -> i32 {
    var total: i32 = 0                // mutable binding (VarStmt): a reassignable local
    loop value: i32 in values {
        total += value
    }
    return total
}

The full binding grammar — let/var, the = and := initializer operators, and binding patterns — is owned by “Statements and Blocks”; the immutable/mutable distinction is grounded in “Permissions and Binding State.”

1.2.2 Local Reasoning

The second principle, verbatim from §0.4:

2. Local Reasoning.
   A reader SHOULD be able to determine the authority, mutability, ownership, copy/move/reference behavior, synchronization behavior, suspension behavior, and dynamic-check behavior of a construct from its local syntactic context and the directly referenced type/procedure signature.

Semantics. Everything that matters about how a construct behaves must be determinable from (a) the construct’s own local syntax and (b) the signatures it directly names — nothing further. A reader must never have to open a third file, trace a chain of definitions, or run the program to learn whether a line acquires authority, mutates, moves, copies, references, synchronizes, suspends, or performs a dynamic check. The properties the reader must be able to recover locally are explicitly enumerated: authority, mutability, ownership, copy/move/reference behavior, synchronization behavior, suspension behavior, and dynamic-check behavior.

Concrete consequences for everyday code:

• Mutability and aliasing are in the type. Permissions (const, unique, shared — owned by “Permissions and Binding State”) prefix the type itself, so the reader sees from a binding’s type whether the value can be mutated and how it can be aliased.
• Move is a written operation. Transferring ownership uses the move form (a prefix move expression, and move argument/parameter modes), so the reader sees ownership transfer at the use site rather than inferring it.
• Copy is a written operation. Duplicating a value uses copy, so the reader sees duplication at the use site.
• Suspension is visible. A suspending operation is spelled with an explicit suspension form (wait, yield, yield from); the reader knows a line can suspend by looking at it. See “Asynchronous Operations.”
• Synchronization is visible. Acquiring authority over shared state uses an explicit key block (%read, %write, %release, %speculative write); the reader sees the synchronization boundary in the source. See “Key System” and “Structured Parallelism.”
• Dynamic checks are opt-in markers. A dynamic class object is written with a $-prefixed type ($ClassName), and runtime-verified scopes are written with the #dynamic attribute, so the reader knows a dynamic check happens here. See “Abstraction and Polymorphism.”

The practical test for Local Reasoning: cover everything except this construct and the signatures it names — can you still answer “does this allocate / copy / move / reference / synchronize / suspend / dynamically check?” If yes, the code honors the principle. If you would have to look elsewhere, the design has failed Local Reasoning.

/// Renders one frame. The signature alone tells the reader:
///   - `frame_index` is an immutable u64 parameter (no permission prefix needed for a bit-copyable scalar);
///   - `surface` is uniquely owned and mutable through this call (the `unique` permission);
///   - the call neither suspends nor synchronizes (no suspension or key form appears in the signature).
procedure renderFrame(frame_index: u64, surface: unique RenderSurface) -> FrameStats {
    let stats: FrameStats = surface.draw(frame_index)
    return stats
}

1.2.3 Explicit over Implicit

The third principle, verbatim from §0.4:

3. Explicit over Implicit.
   Source constructs MUST NOT hide externally observable effects, synchronization, allocation, copying, dynamic verification, suspension, unsafe behavior, or authority acquisition.

Semantics. This is the strongest of the four rules — note that it is the only one stated with MUST NOT rather than SHOULD. A construct is forbidden from hiding any of the enumerated phenomena: externally observable effects, synchronization, allocation, copying, dynamic verification, suspension, unsafe behavior, or authority acquisition. Each of these must be surfaced in the source where it happens. Explicit over Implicit is the prohibition side of Local Reasoning: Local Reasoning says the reader must be able to determine these facts locally; Explicit over Implicit says a construct must not be allowed to conceal them.

Concrete consequences for everyday code:

• No hidden allocation. Region allocation is written as new value for the current scoped region or as a Region@Active handle’s ~>alloc method call for an explicit target. It does not happen silently behind an innocent-looking expression. See “Statements and Blocks” (region grammar, B.14).
• No hidden copy. Copying a value is the written copy operation, not an automatic consequence of using a value twice. Where a value would otherwise be moved, the author writes copy to opt into duplication.
• No hidden synchronization or authority acquisition. Taking authority over shared data is written with a key block; there is no implicit lock.
• No hidden suspension. An operation that can suspend says so through an explicit suspension form (wait, yield, yield from).
• No hidden unsafe behavior. Operations that step outside the safe language live inside an unsafe block, which is a visible lexical boundary. See “Expressions” and “Statements and Blocks.”
• No hidden dynamic verification. Where conformance or dispatch is resolved at runtime, the construct carries an explicit dynamic marker ($-prefixed type or #dynamic scope).

The style guide reinforces this directly. “Source constructs MUST NOT hide externally observable effects” becomes the practical rules “Treat unsafe and [[dynamic]] as deliberate boundary tools, not convenience escapes” and “Keep authority narrow.” The language refuses to let an effect be invisible; the style guide tells you to keep the visible effects minimal.

procedure accumulateStaged(values: [i32]) -> i32 {
    var total: i32 = 0
    region {
        // Allocation is explicit: `new` targets the current scoped region.
        // Nothing in the surrounding code hides it.
        // The allocated value is used inside the region; it does not escape (escaping a
        // region-allocated value is a static provenance error, E-MEM-3020).
        let snapshot: Snapshot = new Snapshot { sum: total, count: 0 }
        total += snapshot.sum
    }
    return total
}

1.2.4 Static by Default

The fourth principle, verbatim from §0.4:

4. Static by Default.
   Where both static and runtime mechanisms are possible, the static mechanism is the default. Runtime checks, runtime synchronization, dynamic dispatch, heap allocation, copying, and foreign trust boundaries require explicit source opt-in.

Semantics. Whenever the language could do something either at compile time or at run time, it chooses compile time unless the author explicitly opts into the runtime mechanism. The runtime mechanisms requiring explicit opt-in are enumerated: runtime checks, runtime synchronization, dynamic dispatch, heap allocation, copying, and foreign trust boundaries. The default for each is its static counterpart: static checks, no synchronization, static dispatch, stack/region storage, move, and the safe-language boundary.

This rule connects directly to the conformance and phase model (§1.1 and §1.5 of the spec; summarized in §1.4 of this chapter). As much verification as possible is discharged statically. The specification fixes which checks are static and which are deferred to runtime. The static/runtime partition from §1.1 “Static vs. Runtime Checks,” reproduced verbatim:

StaticCheck = {PatternExhaustiveness, TypeCompatibility, PermissionViolations, ProvenanceEscape, ArrayBounds, SafePointerValidity}
RuntimeCheck = {IntegerOverflow, SliceBounds, IntDivisionByZero, ShiftRange, CastRange}

RuntimeBehavior(IntegerOverflow) = Panic
RuntimeBehavior(SliceBounds) = Panic
RuntimeBehavior(IntDivisionByZero) = Panic
RuntimeBehavior(ShiftRange) = Panic
RuntimeBehavior(CastRange) = Panic

Pattern exhaustiveness, type compatibility, permission violations, provenance escape, array bounds, and safe-pointer validity are resolved before the program runs. Only the five enumerated runtime checks are deferred, and each one panics on failure. The complete runtime panic taxonomy is owned by “Common Lowering, Program Lifecycle, and Backend” (§24.5.2).

Concrete consequences for everyday code:

• Dispatch is static unless you ask for dynamic. A polymorphic call resolves statically (by monomorphization) by default; dynamic dispatch is opted into with a $-prefixed dynamic class object. See “Abstraction and Polymorphism.”
• Storage is stack/region unless you ask for heap. Values are stack- or region-allocated by default; allocation is explicit (also required by Explicit over Implicit). See “Concrete Data Types” and “Statements and Blocks.”
• Values move unless you ask to copy. The default for using a value is to move it; copy is the opt-in for duplication.
• No synchronization unless you ask for it. Shared-state authority and runtime synchronization are opted into through the key system and structured parallelism.
• Foreign code is a trust boundary you cross deliberately. Calling foreign functions crosses an explicit FFI boundary (extern blocks, foreign contracts). See “Foreign Function Interface.”
• Verification is front-loaded. Because static checking is the default, most of your bugs surface at compile time as diagnostics, not at run time as panics.

// Static by default in action: the generic procedure resolves its callee statically
// by monomorphization. No dynamic dispatch, no allocation, no synchronization is
// introduced implicitly. The bound `<: Eq` is a real foundational class (§13);
// `left.eq(right)` calls its `eq(~, other: const Self) -> bool` method.
procedure areEqual<TValue <: Eq>(left: TValue, right: TValue) -> bool {
    return left.eq(right)
}

1.3 The Mental Model a Developer Should Hold

The four rules combine into a single operating posture. Internalize this and most “how do I write X” questions answer themselves:

1. Assume there is exactly one way, and write that way. Do not look for shorthand. If you find yourself wanting two spellings of the same thing, one of them does not exist (One Correct Way).
2. Make every consequential property visible where it happens. Mutability and aliasing live in the type; movement, copying, allocation, suspension, synchronization, dynamic dispatch, and unsafe operations are each written at their use site (Local Reasoning + Explicit over Implicit).
3. Default to the compile-time, safe, non-allocating, non-synchronizing, static-dispatch, move-not-copy mechanism, and opt into the runtime/heap/dynamic/foreign mechanism only deliberately (Static by Default).
4. Prefer the strongest mechanism the language can check. Push correctness into types, permissions, modal states, contracts, and invariants before reaching for runtime validation. The style guide states this as: “Use the type system, modal types, contracts, invariants, and narrow capabilities before reaching for weaker runtime-only validation.”

The summary slogan: the source text is the specification of behavior. If a behavior is real, it is written; if it is written, it means exactly one thing.

How the philosophy shapes API and module design

The four rules are not only about expression-level code; they dictate how you design types, procedures, and modules. The style guide (AGENTS.md) operationalizes the philosophy into API and module rules:

• APIs are narrow and explicit (One Correct Way + Local Reasoning). “Keep APIs small, explicit, and stable.” “Prefer narrow, specific APIs over broad convenience APIs.” A broad convenience API is, in effect, a set of redundant spellings; the language’s preference for one correct operation extends to a preference for one strong API over many weak helpers: “Prefer a small number of strong, composable types over many weak convenience helpers.”
• Authority is passed narrowly (Local Reasoning + Explicit over Implicit). “Keep authority narrow. Pass only the capabilities and data that are actually used.” “Do not thread through broad ‘god context’ objects for convenience.” When several capabilities genuinely travel together at a real subsystem boundary, define a narrow projected context type for that boundary. Narrow capability passing is what makes a procedure’s authority readable from its signature — directly serving Local Reasoning.
• State lives in types, not booleans (Static by Default). “Prefer state encoded in types over state encoded in booleans.” Use modal types to model lifecycle: “If behavior, available fields, or allowed operations differ by lifecycle state, model that with modal types rather than booleans, comments, or informal conventions.” This pushes a runtime concern (which state am I in?) into a statically checked concern (the type encodes the state). See “Modal and Special Types.”
• Rules the language can express belong in the code (Static by Default). “If a rule about safety, range, state, ownership, lifetime, authority, or valid sequencing can be expressed with contracts or invariants, express it in code.” “Do not leave machine-checkable rules as comments alone.” Contracts and invariants (see “Procedures and Contracts”) convert prose preconditions into static or contract-checked guarantees.
• unsafe, #dynamic, and FFI are boundary tools (Explicit over Implicit). Each is a visible boundary, kept “as small and local as possible,” wrapped in safe APIs that re-establish project invariants, and isolated to dedicated boundary modules in the FFI case. These markers exist because the language forbids hiding the effects they represent.
• Visibility is part of the contract. “Always write visibility explicitly where the language allows it.” “Treat visibility as part of the API contract, not as an optional decoration.” Directories define modules in Ultraviolet; file names are not module boundaries (style guide, “Module Structure”). Keep public module roots stable and reorganize internals freely.

//! Frame submission boundary. This module exposes exactly the authority a caller
//! needs to submit a frame, and nothing more.

/// Submits a prepared frame for presentation.
///
/// Authority: requires unique ownership of the swapchain only; it does not take
/// the device, the asset cache, or any broader context.
/// Postcondition: the returned receipt identifies the submitted frame.
public procedure submitFrame(swapchain: unique Swapchain, frame: Frame) -> FrameReceipt {
    let receipt: FrameReceipt = swapchain.present(frame)
    return receipt
}

1.4 The Language Design Contract (§0.4)

The Language Design Contract is the normative home of the four rules. Its framing sentence and its conformance clause are the binding statements; the four numbered principles (reproduced in full in §1.2 above) are the substance.

The framing sentence and conformance clause, verbatim:

Ultraviolet is a general-purpose systems programming language optimized for
source code written by humans, generated by AI systems, and reviewed by humans.

A conforming design change SHOULD preserve the following principles:

Two normative facts follow from this:

• Scope. The contract governs design changes to the language itself, stated with SHOULD. It is the rule the language designers hold themselves to. As a developer you inherit its results: because the language is built to preserve these four principles, the code you write enjoys One Correct Way, Local Reasoning, Explicit over Implicit, and Static by Default as guarantees, not aspirations.
• Strength gradient. The framing clause uses SHOULD for preserving the principles, and three principles are themselves stated at SHOULD strength (One Correct Way’s no-aliases clause, Local Reasoning, Static by Default), but One Correct Way opens with a MUST (“each semantic operation … MUST have exactly one accepted source form”) and Explicit over Implicit is stated entirely with MUST NOT — source constructs must not hide the enumerated effects. The normative keywords MUST, MUST NOT, SHOULD, SHOULD NOT, and MAY are interpreted per RFC 2119 (§1.3, “RFC 2119 Interpretation”). In practice, the prohibition on hidden effects is the rule you will most often see enforced by a hard compiler diagnostic, while the others shape the available syntax so thoroughly that you rarely encounter a violation to begin with.

The contract connects to conformance through the phase model. A program is conforming exactly when it is well-formed: from §1.1, Conforming(P) ⇔ WF(P), and well-formedness requires that every required judgment over the four translation phases succeeds. The four phases (§1.5, “Compile-Time Execution and Phase Ordering”) are:

TranslationPhases = [Phase1, Phase2, Phase3, Phase4]
Phase1 = ParseAndAggregate
Phase2 = ExecuteComptime
Phase3 = ResolveAndTypecheck
Phase4 = LowerAndEmit

The phase ordering is strict and is itself an expression of Static by Default. From §1.5, the normative ordering is:

1. Phase 1 MUST parse and aggregate all modules before Phase 2 begins.
2. Phase 2 MUST execute all compile-time forms over the Phase 1 module set in the deterministic module order defined by §22.1.5.
3. Any declaration emitted during Phase 2 MUST be incorporated into the module set before Phase 3 begins.
4. Phase 3 MUST resolve names and discharge static semantics against the Phase 2-expanded module set.
5. Phase 4 MUST lower and emit only the program accepted by Phase 3.

The maximum amount of verification is therefore completed before anything runs, and code the static phases reject never reaches the backend. The full conformance algebra and the phase-order judgments are owned by “Conformance and Notation.”

One further design fact you will meet early: the target profile is never inferred from the host. SelectedTargetProfile is resolved from an explicit CLI override, then from toolchain.target_profile in Ultraviolet.toml, and otherwise the invocation is ill-formed — a conforming implementation MUST NOT silently infer SelectedTargetProfile from the host platform. This is Explicit over Implicit applied to the build itself: the target is a written decision, not an ambient default. (Project and build resolution are owned by “Project and Compilation Model.”)

1.5 How the Specification and Handbook Are Organized

The specification is the single normative source of truth, and this handbook tracks its structure. Understanding the organization is itself a practical skill: when you need the exact rule for a construct, you must know where its one normative home is.

1.5.1 Document Organization (§0.1)

Four organizing rules govern the entire specification, verbatim from §0.1:

1. This file is the canonical normative language specification.
2. Each feature section MUST have exactly one normative home in this file.
3. Each leaf feature section MUST use this subsection order:
   - Syntax
   - Parsing
   - AST Representation / Form
   - Static Semantics
   - Dynamic Semantics
   - Lowering
   - Diagnostics
4. Shared framework material belongs only in infrastructure chapters.

Rule 2 is the structural form of One Correct Way: just as each operation has one accepted spelling, each feature has one place where its rules are defined. There is no second, possibly-conflicting description elsewhere. When this handbook says “owned by chapter X,” it is naming that single normative home.

1.5.2 Canonical Chapter Outline (§0.2)

The specification’s canonical chapter list, verbatim from §0.2:

- 0. Front Matter
- 1. Conformance and Notation
- 2. Diagnostic Infrastructure
- 3. Project and Compilation Model
- 4. Source Text and Lexical Structure
- 5. Parsing and AST Infrastructure
- 6. Abstract Machine, Objects, Responsibility, and Authority
- 7. Name Resolution and Visibility
- 8. Type System Core
- 9. Attributes and Metadata
- 10. Permissions and Binding State
- 11. Module-Level Forms
- 12. Concrete Data Types
- 13. Modal and Special Types
- 14. Abstraction and Polymorphism
- 15. Procedures and Contracts
- 16. Expressions
- 17. Patterns
- 18. Statements and Blocks
- 19. Key System
- 20. Structured Parallelism
- 21. Asynchronous Operations
- 22. Compile-Time Execution and Metaprogramming
- 23. Foreign Function Interface
- 24. Common Lowering, Program Lifecycle, and Backend
- Appendix A. Diagnostic Index
- Appendix B. Complete Grammar Reference
- Appendix C. AST Form Index
- Appendix D. Layout, ABI, and Runtime Reference

The ordering is deliberate and pedagogical. It moves from the contract and machinery (conformance, diagnostics, project model, lexical structure, parsing) to the abstract machine and naming (the objects/responsibility/authority model, name resolution and visibility), to the type system and declarations (type system core, attributes, permissions, module-level forms, concrete and modal types, polymorphism), to procedures and the executable surface (procedures and contracts, expressions, patterns, statements), to advanced execution (keys, structured parallelism, async, compile-time metaprogramming, FFI), and finally to lowering and backend. Read in order, each chapter depends only on chapters before it. This handbook follows the same progression; when a chapter forward-references machinery, it names the owning chapter so you can resolve it.

Two appendices are normative-adjacent and you will use them constantly:

• Appendix B (Complete Grammar Reference) consolidates the canonical grammar productions into one parser-oriented reference. Every grammar block this handbook reproduces verbatim comes from Appendix B or from the owning feature section. Note the caveat Appendix B states about itself: the *_attribute productions and certain async and FFI productions are informative shape restatements. Attributes actually parse through the generic attribute production, and each owning section validates argument shape; the async surface forms (B.11) are ordinary class, procedure, and loop syntax. Always treat the owning section as authoritative over an informative restatement.
• Appendix A (Diagnostic Index) is informative only. Per §2.4, Appendix A MUST NOT define a diagnostic’s SpecCode, SeverityColumn, or ConditionColumn. The binding definition of a diagnostic’s code, severity, and condition lives in the owning construct section, never in the index. When you cite a diagnostic, cite its owner.

1.5.3 Required Feature-Section Template (§0.1 / §0.3)

Every leaf feature section in the specification uses the same fixed subsection order. From §0.1, that order is:

- Syntax
- Parsing
- AST Representation / Form
- Static Semantics
- Dynamic Semantics
- Lowering
- Diagnostics

§0.3 defines exactly what each subsection must contain, reproduced verbatim:

Subsection	Required Content
Syntax	Concrete grammar and surface-form restrictions
Parsing	Parse entry points, disambiguation, recovery, feature-local parse constraints
AST Representation / Form	AST forms, invariants, normalized forms
Static Semantics	Well-formedness, resolution, typing, admissibility, compile-time rejection
Dynamic Semantics	Abstract-machine behavior, runtime transitions, observable effects
Lowering	Feature-local IR, ABI, layout, and backend mapping rules
Diagnostics	Diagnostic conditions owned by the feature section

This template is the single most useful map for finding a rule fast. If you need the grammar of a construct, read its Syntax. If you need to know why the compiler rejected your code, read Static Semantics and Diagnostics. If you need the runtime behavior, read Dynamic Semantics. The template also explains why this introduction chapter is intentionally cross-cutting: introductions and philosophy are framework material, and per §0.1 rule 4, framework material lives in infrastructure chapters, not scattered into feature sections.

This handbook’s per-feature chapters mirror the template: each construct is presented with its exact syntax, its precise semantics (static and dynamic), and at least one idiomatic compiling example, with diagnostics called out.

1.5.4 The shape of the surface language

To anchor the rest of the handbook, here are the canonical top-level and type forms from Appendix B, reproduced verbatim. These are grammar you will see fully explained in later chapters; reproduced here so the mental model has concrete syntax attached.

Top-level items (Appendix B.6) — the declarations a module is built from:

top_level_item ::= import_decl | using_decl | static_decl | procedure_decl | comptime_procedure_decl | record_decl | enum_decl | modal_decl | class_declaration | type_alias_decl | extern_block | derive_target_decl

visibility ::= "public" | "internal" | "private"

Visibility is public | internal | private (note the spelling: internal, not crate or mod). The style guide requires writing visibility explicitly wherever the language permits it. These declaration forms are owned by “Module-Level Forms,” “Procedures and Contracts,” “Concrete Data Types,” “Modal and Special Types,” “Abstraction and Polymorphism,” “Compile-Time Execution and Metaprogramming,” and “Foreign Function Interface,” respectively.

The type grammar (Appendix B.2) shows how Local Reasoning is built into types via the permission prefix:

type                ::= permission? non_permission_type refinement_clause?
permission          ::= "const" | "unique" | "shared"

The three permissions are const, unique, and shared — exactly those spellings; they are owned by “Permissions and Binding State.” A type carries its permission so that, per Local Reasoning, mutability and aliasing behavior are visible at every binding.

A complete, minimal, idiomatic program tying the surface together. The executable entry point is procedure main. Its signature is fixed by the specification: main MUST be public, take exactly one Context-bundle parameter, and return i32 (the process exit code). A zero-parameter main is rejected (E-MOD-2431, invalid main signature); a missing main is rejected (E-MOD-2434).

//! Entry module for a small executable.

/// A 2D integer point.
public record Point {
    public x: i32
    public y: i32

    /// Returns the Manhattan distance from the origin.
    /// Reads the receiver immutably (the `~` shorthand is a `const` receiver).
    public procedure manhattan(~) -> i32 {
        return self.x + self.y
    }
}

/// Program entry point. `main` keeps its language-mandated name and required
/// signature: it is `public`, takes the Context capability bundle, and returns i32.
public procedure main(ctx: Context) -> i32 {
    let origin_offset: Point = Point { x: 3, y: 4 }
    let distance: i32 = origin_offset.manhattan()
    return distance
}

This program exhibits the philosophy end to end: one correct binding form per local (let, immutable, move-initialized with =); explicit visibility on every declaration; /// documentation on the public type and method and //! on the module (style guide, “Documentation Comments”); a record for plain value data (style guide, “Type Design”); the receiver shorthand ~ (a const receiver) for the method, with field access written explicitly as self.x and self.y (only self and parameters are in scope inside a method body — fields are not bare names); an explicit return from each non-unit procedure (required — see §1.7 below); and main retained as the language-mandated entry point with its required Context parameter and i32 return type. The record, method, and procedure forms are owned by “Concrete Data Types” and “Procedures and Contracts”; the Context capability bundle is owned by “Abstract Machine, Objects, Responsibility, and Authority” and “Common Lowering, Program Lifecycle, and Backend.”

1.6 Idioms & Best Practices

These idioms are grounded in the four rules and the style guide (AGENTS.md). They are the everyday habits that keep code conforming and reviewable.

• Write exactly one form; do not hunt for shorthand. One Correct Way means the form you find in the spec is the form. Use let for immutable bindings and var only when reassignment is a real requirement (they parse to distinct AST forms and differ in mutability — a genuine semantic difference).
• Put correctness in the type system first. “Use the type system, modal types, contracts, invariants, and narrow capabilities before reaching for weaker runtime-only validation.” Model lifecycle with modal types, not booleans or comments. See “Modal and Special Types.”
• Express machine-checkable rules in code, not comments. “If a rule about safety, range, state, ownership, lifetime, authority, or valid sequencing can be expressed with contracts or invariants, express it in code.” “Express correctness in the code, not in comments.” Contracts and invariants are owned by “Procedures and Contracts.”
• Keep authority narrow. Pass only the capabilities a procedure actually uses; do not thread broad “god context” objects. Define a narrow projected context type when several capabilities genuinely travel together at a real boundary. This directly serves Local Reasoning by making authority readable from the signature.
• Always write visibility, and write explicit returns. “Always write visibility explicitly where the language allows it.” Write explicit return statements in non-unit procedures — this is not merely style: a procedure with a non-unit return type requires an explicit return statement (diagnostic E-TYP-1507), and a procedure declaration requires an explicit return-type annotation (E-TYP-1508).
• Brace control-flow bodies. The grammar parses an if body, an else body, and a loop body as a braced block_expr. Writing if cond { ... } and loop ... { ... } with braces is the form guaranteed to parse. (The style guide permits omitting braces for a single-statement body for legibility; when in doubt, use braces, since the core grammar’s if/loop tails are braced blocks.)
• Treat unsafe, #dynamic, and FFI as deliberate boundaries. Keep unsafe blocks as small and local as possible; wrap them in safe APIs that re-establish invariants; document ownership, lifetime, thread affinity, and caller obligations at every unsafe boundary. Use #dynamic only when semantics are genuinely dynamic, never to bypass static conformance. Isolate FFI to dedicated boundary modules. These are owned by “Expressions”/“Statements and Blocks,” “Abstraction and Polymorphism,” and “Foreign Function Interface.”
• Prefer static and compile-time mechanisms by default. Let the static checks (PatternExhaustiveness, TypeCompatibility, PermissionViolations, ProvenanceEscape, ArrayBounds, SafePointerValidity) catch bugs before runtime; opt into runtime mechanisms only deliberately (Static by Default).
• Name by the matrix. Types PascalCase; procedures, methods, and transitions camelCase; locals and parameters snake_case; constants and statics SCREAMING_SNAKE (private _SCREAMING_SNAKE); private instance fields _snake_case; enum variants PascalCase; generic parameters PascalCase with a T prefix (TValue). Boolean variables/fields are predicate snake_case (is_ready); boolean procedures/methods are predicate camelCase (isReady). Preserve established acronyms (UUID, D3D12Device). See the style guide’s Naming Matrix.
• Document the public surface. Every public module gets //!; every public type, procedure, method, transition, and exported constant gets /// covering purpose, important preconditions, important postconditions, ownership/capability expectations, and notable failure modes (style guide, “Documentation Comments”). Item documentation is ///; module documentation is //!; ordinary comments are //.
• Keep files small and organized by responsibility. Directories define modules; multiple .uv files in a directory belong to the same module; keep files around ~400 lines and split by responsibility, lifecycle phase, or subsystem rather than arbitrary size. Use 4-space indentation, ~100-column lines, and same-line (K&R) braces (style guide, “Formatting” and “Module, Directory, and File Organization”).

//! Session lifecycle, modeled as a modal type rather than boolean flags.

/// A playback session whose available operations differ by lifecycle state.
/// Modeling the lifecycle as `modal` keeps the legal operations statically checked
/// (Static by Default) and visible at the use site (Local Reasoning).
public modal Session {
    @Idle {
        public source: AssetSource

        /// Begins playback. Available only in the Idle state.
        /// `self` is the moved Idle session; its fields are read as `self.source`.
        public transition beginPlayback(start_frame: u64) -> @Playing {
            return Session@Playing { source: self.source, frame_index: start_frame }
        }
    }

    @Playing {
        public source: AssetSource
        public frame_index: u64

        /// Stops playback and returns to Idle. Available only in the Playing state.
        public transition stop() -> @Idle {
            return Session@Idle { source: self.source }
        }
    }
}

This idiom shows the philosophy’s payoff for API design: a caller cannot call stop on an Idle session or beginPlayback on a Playing one, because the transitions belong to the states — the rule is enforced statically by the type, not by a boolean guard or a comment. A transition is invoked with the transition operator (receiver ~> transitionName(args)) and consumes its source-state value by move, producing a value in the target state. The modal, @State, transition, and ~> forms are owned by “Modal and Special Types.”

1.7 Pitfalls & Diagnostics

The following pitfalls are the ones most directly tied to violating the four foundational rules and the style guide. Each is grounded in the specification’s diagnostics and conformance model.

• Expecting a shorthand or alternate spelling that does not exist. Because of One Correct Way, the language deliberately omits aliases and sugar. If you reach for a second spelling of an operation and the parser rejects it, the correct form is the one the spec defines — there is no equivalent alternate. Do not assume a convenience form exists.
• Writing a brace-less if/else/loop body. The grammar’s if_tail and loop body are braced blocks (block_expr ::= "{" statement* expression? "}"). Write if cond { return left } else { return right } and loop ... { ... } with braces. A brace-less if cond return left is not guaranteed to parse under the core grammar.
• Omitting an explicit return from a non-unit procedure. A procedure with a non-unit return type requires an explicit trailing return (diagnostic E-TYP-1507, “Procedure with non-unit return type requires explicit return statement”). Falling off the end of a value-returning procedure body is ill-formed. A procedure declaration also requires an explicit return-type annotation (E-TYP-1508). For unit-returning procedures, @result has type () and an explicit return is not required.
• Writing main with the wrong signature. main MUST be public, take exactly one Context-bundle parameter, and return i32. A zero-parameter main, a non-public main, a generic main, or a wrong return type is rejected: E-MOD-2431 (invalid signature), E-MOD-2432 (main is generic), E-MOD-2434 (missing main), E-MOD-2430 (multiple main procedures).
• Accessing a field by a bare name inside a method or transition. Inside a method or transition body, only self and the declared parameters are in scope; fields are reached through the receiver as self.field. Writing the bare field name resolves to nothing and is ill-formed.
• Letting a region-allocated value escape its region. A value allocated with new or Region@Active~>alloc carries region provenance; returning it (or otherwise storing it in a longer-lived location) is a static provenance escape (E-MEM-3020, ProvenanceEscape). Consume region-allocated values inside the region, or allocate them where they will live.
• Misspelling region as aliasing. A named region is written region as name { ... } (region_alias ::= "as" identifier). region name { ... } does not bind a named region; the region binding is otherwise synthetic and cannot be referenced by user code except as the implicit target of new.
• Assuming the target profile defaults to your host. A conforming implementation MUST NOT infer SelectedTargetProfile from the host platform; if neither a CLI override nor toolchain.target_profile in Ultraviolet.toml provides it, the compilation invocation is ill-formed. Always set the target profile explicitly.
• Expecting a runtime check where the spec defines a static one (or vice versa). The static/runtime partition is fixed (§1.1). Pattern exhaustiveness, type compatibility, permission violations, provenance escape, array bounds, and safe-pointer validity are static — compile errors, not runtime panics. Integer overflow, slice bounds, integer division by zero, shift range, and cast range are runtime checks, each of which panics on failure (RuntimeBehavior(...) = Panic). Do not write code expecting a graceful runtime fallback for a static violation, and do not assume a static rejection where the spec defers the check to a runtime panic. The full panic taxonomy is owned by “Common Lowering, Program Lifecycle, and Backend” (§24.5.2).
• Citing Appendix A as the source of a diagnostic’s meaning. Appendix A is informative only and MUST NOT define a diagnostic’s code, severity, or condition (§2.4). The binding definition lives in the owning construct section. Trust the owner, not the index.
• Treating an informative grammar restatement as authoritative. In Appendix B, the *_attribute productions, the async grammar (B.11), and parts of the FFI grammar are explicitly informative shape restatements; attributes parse through the generic attribute production and each owning section validates argument shape, and the async surface forms are ordinary class/procedure/loop syntax. When an informative restatement and the owning section appear to differ, the owning section governs.
• Hiding an effect to “keep the code clean.” Explicit over Implicit is a MUST NOT: a construct may not hide observable effects, synchronization, allocation, copying, dynamic verification, suspension, unsafe behavior, or authority acquisition. Reaching for unsafe or #dynamic to make an effect disappear, or threading a broad context to avoid naming the capability you use, violates the contract and the style guide. Keep the effect visible and the authority narrow.
• Encoding state in booleans instead of types. Modeling a lifecycle with is_started/is_stopped flags forfeits static checking and pushes a correctness obligation onto runtime convention. The style guide directs you to modal types for state-dependent behavior; doing otherwise is a design pitfall even when it compiles.
• Modeling the pipeline backwards. The phases are strict (§1.5): compile-time forms execute in Phase 2 over the fully aggregated Phase 1 module set, and any declaration they emit is incorporated before Phase 3 resolves names and types. Code that assumes name resolution or typing has happened before compile-time expansion is modeling the pipeline backwards. Phase 4 lowers only what Phase 3 accepted. Compile-time forms are owned by “Compile-Time Execution and Metaprogramming.”

Across all of these, the diagnostic infrastructure renders errors with a code, severity, message, and span. Diagnostic codes follow the DiagPrefix "-" DiagCategory "-" DiagDigits format from §1.3 — DiagPrefix ∈ {E, W, I, P}, DiagCategory is three uppercase letters, and DiagDigits is four digits (for example, E-TYP-1507). The prefix tells you immediately whether the compiler rejected the program statically (E), is warning (W), is informational (I), or is reporting a runtime panic condition (P). The diagnostic machinery is owned by “Diagnostic Infrastructure,” and the per-feature diagnostics are owned by each feature’s chapter.