Different parts of the Topaz product answer different questions. Use the language definition to decide what a program means, the checker to decide whether a source file is admitted, and execution evidence to decide what was observed in a particular environment.
Which authority answers which question?
| Authority | What it establishes | What it does not establish |
|---|---|---|
| Language specification (SPEC) | Canonical syntax, types, semantics, and observable language boundaries | That an implementation has no bugs, or that every output target supports every feature |
| Checker | Whether this source parses, resolves, type-checks, and is admitted for the selected use | Runtime behavior, output equivalence, or correctness of an external program |
| Interpreter and output targets | Direct behavior or a generated product for a selected target; unsupported target behavior must be rejected clearly | Identical generated internals, identical performance, or universal target support |
| Canonical examples | One supported form or workflow with an observable result | Exhaustive coverage or permission for syntax that the specification does not define |
| Tests and verification receipts | What happened for named inputs, toolchains, environments, profiles, and limits | Formal verification, whole-language parity, or proof that no divergence exists outside the recorded experiment |
A practical verification path
- Start from the current language pages and canonical examples.
- Run
topaz checkto catch syntax, name, type, and selected-profile errors. - Run the program and its tests. Record the outputs, diagnostics, file changes, and exit status that matter to the application.
- Build the intended output target and check its documented limits. A target that cannot preserve required behavior must fail clearly.
- When reading a test result or receipt, keep its exact inputs, environment, and limits attached to the claim.
The common command sequence is:
topaz check main.tpz
topaz run main.tpz
topaz build main.tpz --out-dir build
Comparing compiler evidence
Canonical compiler observations let two runs compare named boundaries without
claiming more than the selected evidence establishes. Use semantic for the
ordered source-set through diagnostic and outcome phases, generated-source
for exact emitted Rust, provenance for producer identity, and
native-binary for exact same-target executable bytes. Equality in one layer
does not imply equality in another, and a passing workload is bounded evidence,
not proof of whole-language equivalence.