Program checking

This specification owns acceptance: what a checked program is proved to satisfy before it runs, what checking reads, the discard rules, exhaustive matching, and that every compiler finding is an error.

The rules a checker enforces live with the surfaces they govern. grammar.md owns source forms and the formatter; types.md owns types, visibility, constructor resolution and the data-type category; effects.md owns !tool; semantics.md owns evaluation; errors.md owns Result, ? and faults; modules.md owns imports and versions; tools.md owns what crosses a Tool boundary. This file states what acceptance proves and never gives one of those rules a second meaning. What a diagnostic is, its principles, shape and codes, are runtime/spec/diagnostics.md's.

What acceptance proves

A checked program has one meaning, and these hold for it:

• It is well formed. The source is valid UTF-8 with no bidi control characters and parses under grammar.md.
• It is closed. Every import resolves to one module, the program uses one std and one version of each repository, and there is no cycle across repositories (modules.md).
• Every name resolves to one thing. No bare constructor is ambiguous, no local name matches an import, and no type or function name the prelude exports is declared again (types.md, modules.md).
• Every expression has one type, under types.md's rules with no subtyping. Every type argument is decided by inference over the whole function body or by an annotation.
• Every function's effect is honest. A function with no !tool makes no Tool call, directly or through anything it calls, and a function-typed parameter marked !pure receives only pure functions (effects.md).
• No value is lost by accident. Every statement is Unit, every binding is used, and every match is exhaustive (discarding values, exhaustive matching).
• Control is type-correct. return stands inside a function; an if without else is Unit or Never; a guard's else block cannot fall through; ? appears only in a function returning Result, with error types that match or a converter that makes them match (semantics.md, errors.md).
• Only data goes where data is required. ==, ordering and interpolation apply only to data types; a Tool's arguments and a run's input and output are data; nothing decoded, from a Tool reply, a run's input or json.decode, is or contains an opaque type; functions and tasks never cross (types.md, tools.md).
• Its outside surface is known. Every @tool function the program can reach is listed before it runs (tools.md).

Acceptance does not prove that a run terminates or stays within a host's limits, that a Tool implementation exists, is available, safe, truthful, authorized or affordable, that a reply will have the declared shape, or that a Text value is a safe path, address or prompt. Those are checked when the run meets them, or belong to the host and application around it (what is left to the run).

Checking reads only the program

Checking is a function of:

• the source of every module the program reaches, at the commits its imports resolved to;
• the std version the program uses.

Nothing else is an input. Bindings, implementations, flow-tool.toml, host configuration, credentials, environment variables, replies and histories do not take part, and no checking rule reads them. Fetching remote modules and choosing commits happen before checking (modules.md); the checker consumes their result and contacts no Tool.

Checking the same inputs always gives the same verdict and, for an accepted program, the same program identity (history.md). Formatting is not checked: source the formatter would change is still accepted and means the same.

Whether a function can start a run (semantics.md) is checked when a run names it, against the same checked program.

Discarding values

Three rules decide whether a value may be thrown away. They are the same for every type, with one exception for tasks.

1. No implicit discard. Every statement in a block has type Unit. A value of any other type is dropped only explicitly, with let _ = e, which is the one spelling. let _ = e cannot drop a value that holds a task, anywhere in its type: a dropped task can only be stopped when its owner returns, so its work may never happen (concurrency.md). It is awaited, stopped, kept, or detached with task.detach, which says in the code that it runs until its owner returns.
2. No unused bindings. A name bound by let, by a pattern or as a parameter is mentioned somewhere in its scope. _ marks a parameter or a part of a pattern as not needed.
3. Exhaustive matching. Every match covers every value of its subject's type (below).

send(message)                      // error: Result<Unit, ToolProblem<SendError>> is not Unit
let receipt = send(message)        // error if receipt is never mentioned
let _ = send(message)              // explicit, visible in review, recorded in history
match send(message) {              // handled
    Ok(()) => (),
    Err(problem) => report(problem),
}
list.fold(items, 0, flow(total, _) = total + 1)

Only a task carries a requirement to be used, and no rule knows about Result, Err or Tool replies. The three rules are enough to keep a Tool failure from slipping through by accident:

• Using a result means facing its error. The success value sits inside a Result, and reaching it takes an exhaustive match, guard let or ?.
• Not using a result is visible. The only way to drop it is let _ =, in the source where a reviewer reads it.
• Nothing escapes the record. Every Tool call and its outcome is in the run's history, including outcomes the program dropped (history.md).

No rule can force good handling, only visible handling. Dropping a call's result never makes the call pure (effects.md).

Exhaustive matching

• A match covers its subject's type. For every value of that type, some arm's pattern matches. Guards do not count: an arm with if cond covers nothing for this purpose, so a guarded arm is followed by arms that cover what it may decline.
• Every arm can be taken. An arm whose pattern only matches values that earlier unguarded arms already match is an error.
• A pattern in let or a parameter always matches its type, since there is no other arm to fall to. guard let exists for a pattern that may fail (semantics.md).

Coverage is decided over constructors, tuples, list lengths and literals. A constructor with a field of type Never builds no value, so a match need not name it, though an arm may: match clock.now() { Ok(t) => ..., Err(NotRun(r)) => ..., Err(Unknown(r)) => ..., Err(BadReply(r)) => ... } covers its type. Literal patterns over Int, Decimal or Text never cover their type alone, so such a match ends with a pattern that matches anything. A pub enum exposes all its constructors, so a match outside its module can name them all; a pub opaque type exposes none, so a match outside its module on such a value uses a pattern that matches anything (types.md).

Errors only

A program is accepted only if the compiler reports no error, and everything the compiler reports is an error that refuses it. A compiler may build placeholders after an error so that checking continues and finds more, but it never accepts a program from them and never gives invalid code a meaning. Changing a message's wording never changes whether a program is accepted.

Beyond its errors, a check reports facts tooling shows: the @tool functions a program can reach (tools.md), each function's inferred requirements and effect (effects.md, types.md), and the tail calls where a checkpoint can be taken (history.md). None of these is a diagnostic, and none changes the verdict.

What an error is as data — one pass, no warnings, stable codes, messages, notes and exact fixes — is runtime/spec/diagnostics.md's.

Rules key on categories, not names

The checker knows mechanisms and categories, never particular names. Everything it treats specially, such as the result type a Tool call returns, the optional type, the never type, the operator functions and the type each literal builds, is declared in std and marked @lang (stdlib.md); only std may use it (modules.md). A program's own type with the shape of Result is an ordinary type and gains none of Result's rules.

What is left to the run

Some facts exist only when a program runs, and the run checks them against the checked program without adding a typing rule:

• a run's input decodes into the entry's parameter types, or the run is refused (semantics.md);
• every @tool function the program can reach is bound before the run starts, or the run is refused (tools.md);
• every reply is checked against its declared type, and one that does not match becomes BadReply (tools.md, errors.md);
• the operations that can fault, and host limits, fault when they are reached (errors.md);
• replay checks every call against the record (history.md).

A host may also refuse to start or continue a run under its own policy, such as asking before it first runs a repository's Tool implementation (execution.md). Such a refusal is the host's decision, not a language verdict, and it names the host rule that made it.

Serves foundations: Typed, composable crossings, Visible outside influence, and A general core, bounded in scope.