Appendix E: Execution and verification guide
Do not treat every failure as the same problem. Separate the command's purpose from the stage that failed. A green checking indicator alone does not establish the behavior you intended.
E.1 Choose a command by purpose
| Purpose | Starting point | What remains after success |
|---|---|---|
| Check types, effects, ownership, and proofs | tauto check FILE | Actual I/O, external code, and execution on the target backend |
| Inspect unfinished proofs | tauto goals FILE | Fill each hole and recheck the whole file |
| Check a proposed hole replacement | tauto try FILE --hole NAME --with 'TERM' | Other holes or declarations may still be unfinished |
| Write a checked candidate | tauto fill FILE --hole NAME --with 'TERM' | Inspect the diff and recheck; fill changes the file |
| Inspect actual behavior | tauto run --tote . | Expected results for other inputs and error paths |
| Run tests | tauto test . | Unspecified cases, general properties, and other backends |
| Find names and theorems | tauto library FILE | Required types and assumptions at the call site |
| Format code | tauto fmt FILE | Type correctness and program meaning; formatting is not verification |
See Chapter 12 for details. Execution and tests can run external code. Do not run untrusted sources on the assumption that the CLI is a secure sandbox.
E.2 Isolate the failing stage
- Syntax and names: start with the first diagnostic. Later type errors can follow from an earlier parse or name-resolution failure. Compare filenames and imports with the example.
- Types, usage rules, and effects: distinguish mismatched types, use after move, borrowing, and unhandled effects. Do not replace code with axioms or external functions merely to silence diagnostics.
- Proofs: inspect goals for remaining holes and write down their assumptions and conclusions. If
Reflfails, ask whether both sides agree by computation or require an equality proof. - Execution: use a checked minimal example and distinguish inputs, expected output, and observed output. Printing with
showis not an assertion. - Backend and host: when changing execution targets for the same source, record the build and runtime result separately for each. Success on one does not establish success on another.
E.3 What to keep in a minimal reproduction
- The CLI version and complete command.
- A self-contained failing source, required imports, and manifest, without secrets or business data.
- The expected result, actual diagnostics or output, and exit code.
- Backend and host, plus any external functions or required host capabilities.
- Which of checking, tests, building, and running passed, failed, or were not attempted.
Different stages can report errors together, such as failed type-name resolution followed by a result-type mismatch. Do not assume the later diagnostic is an independent defect; check whether it persists after removing the earlier failure.
E.4 Recorded checks and new observations
Book examples carry build-time checking records. If the content, expected diagnostics, CLI, and records no longer agree, site generation requires rechecking. An old success badge is not evidence for new code.
These records do not establish success in the reader's environment or equivalence across all backends. A proof depending on an axiom is conditional on that assumption. See Chapter 20 for the trust boundary.