Feature contract: do#

1. Lexical and grammar rules, including precedence and termination#

(do EFFECTS RESULT (NAME <- COMPUTATION) (COMPUTATION) ... (return VALUE)) is a parenthesized prefix form. A named step may state a quantity as (QUANTITY NAME <- COMPUTATION); the short form defaults to unrestricted. The final (return VALUE) is structural and mandatory.

2. Scope and binding rules, including generated names#

A named result is in scope in later steps and the final value. It is absent from its own computation. Anonymous steps receive inaccessible internal names, so they cannot capture or be referenced by source.

3. Type and quantity requirements#

Every step must synthesize Computation EFFECTS A for exactly the declared row. The final value checks against RESULT. Explicit result quantities are carried by the continuation lambda; the trusted kernel rejects a linear result used zero or multiple times and an affine result used multiple times.

4. Effects, totality, and evaluation-order rules#

Steps run exactly once, from top to bottom. A failed step stops later steps. The form neither reorders nor weakens rows. Existing whole-file operations close descriptors and remove temporary write files; the failure fixture traces that cleanup. No general scoped-resource construct is introduced.

5. Elaboration into existing core or a specifically versioned new core extension#

do emits nested existing RBind nodes with one final RReturn. Every bind uses the same declared effect row and result type. The kernel accepts the continuation's declared quantity and checks its usage.

6. Representation and target support, where relevant#

Erasure and x86-64 compilation see only existing bind, return, and effect operations. The copied native-emitter fixture proves byte-identical outer ELF and emitted inner ELF against the explicit bind staircase.

7. Error codes and primary/secondary origins#

ALPHA-DO-MISSING-RETURN identifies a closed form without its final return; ALPHA-PARSE-DO identifies an unterminated form. A step with another row gets ALPHA-EFFECT-ROW-MISMATCH at that step. Existing type and quantity codes apply to computations, result values, and continuation use.

8. Formatting and migration rules#

Canonical formatting keeps one step per line and preserves comments. Expanded inspection prints nested bind, continuation lambdas, and return. No automatic bind-to-do migration is registered because arbitrary continuation lambdas may encode scopes that the readable form cannot express.

9. Positive, negative, execution, and edge-case tests#

tests/language/sequencing/ covers explicit/readable core identity, named and anonymous steps, row mismatch, missing return, linear duplication, ordered noncommuting writes, one-effect/one-trace behavior, first-failure stop, cleanup, the copied NativePhysicalEmitProbeFast emitter staircase, and an Alpha-authored parse/lower/resolve/infer fixture (SelfHostedDoParser.alpha). debug/sequence-format-check.py records exact native traces and byte digests.

10. Compatibility with the old edition, serialized forms, and cache keys#

alpha-2026 rejects do; alpha-2027 admits it. Expanded bind/return source remains old-edition compatible. The surface-AST checkpoint codec reserves tags 28--30 for the structural DoBlock/DoStep/DoReturn representation. No checked-core, ALRI, checked-interface, object, or receipt schema changes are made; edition identity prevents cross-edition cache reuse.