Sol's spec review

← Spec review
D — VibeLang has a coherent continuation machine, but its source-language rules admit a demonstrated type error, leave binding hygiene unprotected, violate module expectations, and multiply evaluation strategies behind ordinary call syntax.

Reviewer: sol. Reviewed 2026-10-27. Scope: all 33 files in spec/design/src/ (66,656 words), including the user model, rules, machine, tooling, decisions chapter, and appendices; the relevant entries and amendments in DECISIONS.md; focused read-only implementation checks; and 13 small probe directories under this review's probes/. No other reviewer's work or audit reports were read.

This is a grade for a language design document, not for implementation progress. The runtime core earns substantially more credit than the source semantics. The passing criterion is that a compiler writer can derive binding, evaluation, typing, and interoperation behavior without inventing policy or choosing between contradictory rules. This document fails that criterion. “All rules are decided” is not a substitute for complete, mutually consistent rules.

The owner's diagnosis is partly right. The specification creates several of the bug classes, and explicitly chooses some of the bad behavior. However, Chapter 13 already requires left-to-right, once-only evaluation, short-circuiting, and preservation of method receivers. A compiler that evaluates an operand twice, tests the returned Effect object instead of a running call's success value, or reorders calls violates that specification. Those bugs must not be excused as gaps.

## The call-semantics inventory and the proposed minimal design

**Verdict: F for the call design against the stated principle.** The heading “One syntax, several meanings” accurately describes the problem. Types select execution, quotation, callback representation, and evaluation phase. Names and declaration provenance select additional behavior. The compiler is doing language elaboration during overload resolution, rather than checking a previously determined evaluation strategy.

“Types decide” is not itself a theorem of unsoundness. Statically elaborated languages can be sound. Here it makes a semantics-preserving refactoring, such as extracting a type alias or adding an export to a dependency, capable of changing execution policy. The document needs to justify each such change as language behavior, not as a checker convenience.

The table distinguishes observable source behavior from code-generation mechanisms. A direct shortcut and a generator are not two legitimate source meanings; the specification owes them equivalence.

For the proposed column: **S** means strict VibeLang application with one computation convention; **P** means an explicitly written program thunk; **J** means an explicitly delimited TypeScript hatch; **N** means ECMAScript construction. Adapter names below are illustrative proposed library names.

| Semantics/form | How it is dispatched today | How it should be | Programs that change |
| --- | --- | --- | --- |
| Ordinary VibeLang call f(args) | Inferred control class, E/R, annotation, expected method type; Chapters 13–15 | S: evaluate callee/receiver and arguments once, then enter the callee computation | No direct-style sequencing change |
| “Pure” or synchronous direct call | Body analysis and E = R = never; sometimes a plain annotation | S with an equivalent optimization; representation must not alter behavior | Only programs relying on an optimization bug |
| Imported TypeScript Effect-returning function | Instantiated return type must be Effect itself | Import/adapt once as a VibeLang computation; subsequent calls use S | Raw foreign imports need an explicit adapter declaration |
| Imported plain TypeScript function | Package provenance, JSDoc trust and @throws, lexical execution context | An explicit declaration adapter or J; the call does not infer an FFI policy | Unadapted calls and implicit blanket trust change |
| Plain-annotated VibeLang helper | Annotation opens a plain region that may call untrusted TypeScript without a boundary; Chapter 15 | Plain annotation restricts effects; it does not silently establish trust | Helpers using this implicit escape need J or a declared adapter |
| Call returning Exit/Config/key/error versus Effect | Static identity of instantiated result type, although the same runtime object can inhabit both | Return values are values; only an explicit run operation executes a raw Effect value | asExit()/asEffect() no longer have different implicit unwrapping |
| Effect value p() | Non-function callee's static Effect type | run(p), an ordinary computation primitive; p() requires a callable | Clock.currentTimeMillis(), Config calls, and similar value-calls change |
| By-name argument f(work()) | Candidate's declared parameter type; selected exceptions use instantiated types | P: f(() => work()); strict argument evaluation is unchanged | retry(fetch(id), policy) becomes retry(() => fetch(id), policy) |
| Program lambda/function value | Expected Effect/function/union type chooses plain function, Effect function, or materialized Effect | A lambda is always a computation function; an explicit adapter materializes an Effect | Automatic function-to-Effect conversions become explicit |
| Arrays/records/iterables of programs | Expected element/field/iterated type; recursive conversion helpers | Collections contain explicit P values; a combinator adapter owns conversion | all([a(), b()]) becomes all([() => a(), () => b()]) |
| Annotated Effect const | Written annotation holds the initializer; inference/assertion alone does not | Explicit program construction or ordinary strict Effect factory call, independent of variable annotation | Adding/removing an annotation stops changing evaluation |
| Effect factory | Declared return contract plus the shape/type of returns and whether A accepts them | Explicit factory declaration/adapter; ordinary computation bodies remain cold behind their ABI | Annotated functions inferred to be factories need an explicit marker |
| Callback into an Effect API | Candidate's uninstantiated parameter type, constraints, inferred eligibility, overload ordering | S callback convention selected by an explicit adapter/API contract | Ambiguous callbacks need an explicit adapter |
| Callback into JavaScript, e.g. map | Expected plain callback type; eligibility analysis; foreign callbacks may return Effect as data | J/plain callback explicitly checked for the JavaScript convention | Ineligible callbacks still fail; ambiguous ones become explicit |
| Inline callback parameter versus named type alias | Only an inline function type gains E/R parameters; Chapter 16 | Canonical expanded type and explicit row parameters determine polymorphism | Extracting an alias becomes behavior-preserving |
| Function-or-Effect destination | Parameter count, plain eligibility, and expected union type; Chapter 13 | Separate function and program adapters/overloads distinguished by explicit source forms | Zero-argument handlers must identify their intended form |
| Native methods | JavaScript member reference, with additional Effect result unwrapping | S/J reference application; capture receiver and callable before arguments | Raw Effect-returning foreign methods require adaptation |
| Service member S.method()/service S() | Resolved Context-key shape; member precedence; special class calls | Explicit service lookup use(S), then S application of the returned member | S.method(x) becomes use(S).method(x); S() becomes use(S) |
| Control-operation method | Control declaration and handler evidence | Ordinary S-callable operation wrapper whose body performs a primitive | Surface call syntax can remain |
| Synthetic data methods x.map(...) | Declaration file location, receiver type, missing own member, first parameter's spelling, exception table | Explicit extension-function metadata resolved by symbol, or Module.map(x, ...) | Accidentally recognized methods need an explicit module call |
| Hack pipe topic | Expected parameter position chooses value or by-name expression | Strict value topic, computed once before the body; P is written explicitly | Program pipelines start from a thunk |
| pipe(...) and .pipe(...) | pipe looks ahead into stage signatures; .pipe is the receiver's actual member; running call's A may have no pipe | Ordinary strict calls on explicit values/P; no signature look-ahead | pipe(() => f(), ...) remains possible through the adapter |
| sync / try / callback | Recognized hatch plus first argument's syntax/type; async recognition and declared parameters affect signal injection | J is explicit; code/input/mapper positions and callback convention are fixed | Ambiguous signal/mapper forms need explicit forms |
| trusted(impl, [Errors]) | D249 value-level wrapper, alongside the still-documented JSDoc path | Explicit declaration adapter with one published ABI | JSDoc users migrate once if this is the chosen policy |
| Block after a call | Last argument unless an Effect dual's program position is selected | Explicit trailing P argument with a fixed grammar, not inferred insertion | Dual-position block sugar changes |
| new C(args) / data/error constructors | new always constructs; constructors/accessors/defaults cannot run Effects; data constructors are trusted plain calls | N with strict S evaluation of surrounding argument expressions; constructor body is J/plain | No hidden unwrapping or suspension in construction |
| Generated wrappers and TypeScript callers | Public Effect ABI, private direct ABI, factory exceptions, plain annotation | One exported ABI matching .d.ts; private variants prove the same observations | No user-visible choice by inferred representation |
| Runner calls and generated main | Resolved runner symbols in Chapter 13; spelling-based suppression in D135; exported main and platform-import rules | Explicit resolved runner/entry syntax; ordinary aliases remain ordinary | A user function called runSync stops suppressing main |
| Producer calls and iteration | function* syntax constructs lazily; for...of selects producer/Stream/iterable by static type | Producer introduction stays explicit; iteration adapters have one published pull/close protocol | Implicit cross-fiber Stream adaptation must become visible where it affects handlers |

### A minimal design that retains direct style

Use **one strict application rule in VibeLang computations**, a separately delimited JavaScript rule inside TypeScript hatches, and ECMAScript's existing new syntax. Program construction is explicit and is not another interpretation of application.

1. Every VibeLang computation function, including a pure helper, has the same semantic callable convention. f(x) evaluates its callable reference and x once and executes that computation on the current fiber. A compiler may specialize the representation, not its meaning.
2. () => body always constructs a function. retry(() => fetch(id), policy), fork(() => work()), and all([() => a(), () => b()]) explicitly defer work. A combinator's VibeLang adapter converts these thunks to Effect programs at the boundary. No expected type quotes a call or turns a function value into an Effect.
3. Raw Effect values are data. run(p) explicitly executes one. Imported Effect-returning APIs are adapted once to computation functions; no application tests whether its result type happens to be Effect rather than Exit.
4. sync/try/callback delimit JavaScript and establish an explicit foreign callback convention. A declaration-level trusted adapter can amortize this cost. Trust is attached to a resolved adapter, not inherited from a package name or the fact that another function returned it.
5. An exported VibeLang computation has one TypeScript-facing Effect-returning wrapper. A library consumer may rely on the wrapper's coldness and the phase table below. Exported factories are explicitly identified. Private shortcuts remain compiler implementation details.
6. Service lookup and running an Effect are ordinary named primitives with fixed contracts. Constructors, pattern forms, providers, masks, and control operations have grammar-defined rules; a user binding's spelling never selects them.

This preserves the main goal: inside computation bodies, const user = fetch(id); send(user) still reads as synchronous code. The language change is concentrated at quotation, raw Effect values, and foreign declarations. It does not require an await on every VibeLang call.

The [Eff tutorial's value/computation distinction and handler typing](https://www.eff-lang.org/handlers-tutorial.pdf) provide a small formal starting point. [Koka's effect-polymorphic function application](https://koka-lang.github.io/koka/doc/book.html#sec-polymorphic-effects) demonstrates that direct style and explicit computation types do not require expected-type-dependent argument evaluation.

## Findings, ranked

### 1. BLOCKER — Handler answer types knowingly fail preservation

**Location/rule.** Chapter 9, “The full API”; Chapter 28, “Diagnostics,” EK2119; DECISIONS.md D97:

> “a clause's return computed from it stays out of its type, and EK2119 warns when that return does not fit.”

> “a resume still waiting can receive a value outside its type”

**Position.** A warning cannot make an incorrect static type correct. All resumptions of the same deep handler must return its answer type, including answers produced by later invocations of the same clause. The type-preservation obligation is elementary: a number-typed expression cannot evaluate to a string in a program that used no cast, any, untrusted FFI, or malformed input.

**Confirmed.** [handler-answer/src/main.vibe](probes/handler-answer/src/main.vibe) performs Step.next twice, then returns 1. Its clause writes const n = resume(); return n.toFixed(1). It compiles with only EK2119. The inner clause returns "1.0"; the outer resume is typed number but receives that string. Runtime: TypeError: n.toFixed is not a function. COMPILE_EXIT=0, RUN_EXIT=1. Adding an explicit number annotation to n produces TS2322; that partial defense does not repair inference.

**First principles/prior art.** Answer-type consistency is a handler typing rule, not an inference preference. In [Pretnar's Eff typing, Figure 6](https://www.eff-lang.org/handlers-tutorial.pdf), the continuation and every clause share the handler's output computation type. A restricted annotation requirement is preferable to an unsound approximation.

**Exact replacement rule.**

> Every non-tail resume has the answer type H of the entire handled statement or handle expression, including the results and effects of all clauses and onReturn. Every clause result must be assignable to H. If H cannot be inferred without a cycle, require a written answer contract and reject the program until one is supplied. An incomplete approximation of H is never exposed to an expression that reads a resume result. EK2119 is an error.

**LANGUAGE CHANGE:** yes; the confirmed crashing program is rejected. Confidence: certain.

### 2. BLOCKER — Expected types choose evaluation strategy and result unwrapping

**Location/rule.** Chapter 5, “The one rule”; Chapter 13, “How program values are spelled” and “Calls run Effect itself”:

> “A call runs where it stands, except where a parameter expects a program”

> “as a program that evaluates the expression on each run, as if () => preceded it”

> “only when the call's instantiated type is Effect<A, E, R> itself”

**Position.** The document makes strict evaluation and call-by-name two meanings of the same expression, then adds a third, initializer-holding rule that calls a factory once rather than quoting it. A fourth rule makes structurally related return types choose whether an identical result object executes. These are deliberate source-language semantics; treating them as automatic removal of boilerplate understates their cost.

For example, retry(capture(input), policy) repeats construction and snapshots each attempt, while const p: Effect<number> = capture(input); retry(p, policy) constructs once. The latter is specified, but the caller must know annotation-directed staging in addition to ordinary calls. Extracting an argument into a variable is not generally equivalent.

**Confirmed distinction.** [type-directed-run](probes/type-directed-run/src/main.vibe) defines two TypeScript functions returning Exit.succeed(42), one declared Exit<number>, the other Effect<number>. Identical runtime results become an Exit value and the number 42 respectively. Output: [Success(42),42]. This follows the spec; it is not a compiler misclassification.

**Prior art.** ECMAScript [EvaluateCall](https://tc39.es/ecma262/multipage/ecmascript-language-expressions.html#sec-evaluatecall) fixes reference and argument evaluation before application. TypeScript overload resolution chooses a type; it does not normally change argument execution. Chapter 13 also says “TypeScript tries candidates in declaration order,” but the prototype's TypeScript checker and the inspected Go fork both reorder specialized literal signatures ahead of others (Go checker.go:9194, reorderCandidates). If D56 is retained, its candidate ordering must be specified accurately before using it to select runtime representations. [The TypeScript checker](https://raw.githubusercontent.com/microsoft/TypeScript/refs/tags/v5.9.3/src/compiler/checker.ts), especially reorderCandidates and chooseOverload, is therefore not a sound substitute for an independent source evaluation rule.

**Exact replacement rule.**

> Application always evaluates its callable reference and arguments strictly, once, in source order. Expected types, overload selection, type assertions, generic constraints, return-type widening, and variable annotations do not quote or execute expressions. Delay is expressed by a function literal. Raw Effect values run only through the explicit run operation. An imported Effect-returning function is adapted at a declared boundary before ordinary computation application.

The inventory gives the associated migrations.

**LANGUAGE CHANGE:** yes, substantially; the smallest useful simplification is deleting D147's implicit quotation, D269's annotation-selected staging, and D24's implicit result elimination together. Confidence: certain about current behavior; this is an explicit design recommendation, not a claim that type-directed elaboration is inherently impossible.

### 3. BLOCKER — Built-in patterns and entry detection deliberately use spelling

**Location/rule.** Chapter 1, “What is in scope”; Chapter 13, “Where programs start”; Chapter 29 D208; DECISIONS.md D135:

> “An import or local declaration with the same name shadows a prelude name”

> “The compiler recognizes runners by their resolved symbols”

> “a shadowing local is not consulted”

> “any call of a function named runMain, runPromise, runFork, runSync, or runCallback”

**Position.** These rules cannot coexist as one lexical language. Alpha-renaming a local binding must not turn a predicate into a built-in matcher or disable module startup. The issue is symbol identity, not whether recognizing a few names is convenient.

**Confirmed.** [shadow-pattern](probes/shadow-pattern/src/main.vibe) defines its own Option.Some predicate. Matching 7 against it is rewritten toward isSome and rejected with TS2551. [shadow-runner](probes/shadow-runner/src/main.vibe) defines an empty plain runSync, calls it at top level, and exports main. Compilation and execution both exit 0, but main never runs; the generated entry statement is absent.

**Prior art.** Scheme's binding-aware auxiliary identifiers are the direct precedent. ECMAScript's [ResolveBinding and environment records](https://tc39.es/ecma262/multipage/executable-code-and-execution-contexts.html#sec-resolvebinding) likewise give names meaning through their bindings.

**Exact replacement rule.**

> A special treatment of an identifier or member applies only after resolution to the designated intrinsic symbol, following import and re-export aliases. A local binding shadows the intrinsic completely. Built-in pattern adapters recognize the resolved Option, Exit, Result, and primitive-constructor symbols; other matcher values use the ordinary matcher protocol. Entry suppression occurs only for a resolved recognized runner, never for a function whose text has a runner's name.

Experimental must obey this rule too; D313 correctly says it is shadowable. Exporting main is a documented entry convention; it is not permission to classify unrelated calls by spelling.

**LANGUAGE CHANGE:** yes for D208/D135; restores the shadowing model advertised in Chapters 1 and 13. Confidence: certain.


### 4. BLOCKER — Inline modules mandate snapshot exports while promising TypeScript modules

**Location/rule.** Chapter 10, introductory interoperation promise; Chapter 11's module escape; Chapter 28 EK4408; DECISIONS.md D283/D303:

> “shares its types, modules, and Effect”

> “checked and compiled as a .ts file would be”

> “an import from it reads its exports once, when it has run, so a later assignment to an exported let is not seen”

**Position.** D303 is an explicit semantic defect, not an unspecified optimization. A frozen object of export values and destructuring constants do not implement an ECMAScript module. Freezing the namespace object does not freeze exported bindings. A module escape cannot simultaneously promise ordinary TypeScript and change its central binding semantics.

**Confirmed.** [module-live/src/main.vibe](probes/module-live/src/main.vibe) imports count and bump from an inline module, records count, calls bump, then reads count. It prints [0,0]. ECMAScript imports observe [0,1]. No cast or concurrency is involved. D303 also deliberately moves evaluation after all external imports and equates module names differing only in case; these are additional semantics, not harmless representation choices.

**Prior art.** ECMAScript [Module Namespace [[Get]]](https://tc39.es/ecma262/multipage/ordinary-and-exotic-objects-behaviours.html#sec-module-namespace-exotic-objects-get-p-receiver) reads the exporting environment's current binding. The [TC39 module-declarations draft](https://tc39.es/proposal-module-declarations/) builds on module records, not snapshots.

**Exact replacement rule.**

> An inline module has the binding and evaluation semantics of an ECMAScript module. Named imports, namespace imports, and re-exports refer to live export bindings, including mutable bindings and aliases. Lowering preserves initialization order, temporal dead zones, cycles, side-effect-only imports, and top-level-await dependencies. Module identifiers are case-sensitive. An implementation unable to preserve one of these properties rejects the unsupported construct; it never substitutes a snapshot or silently elides a requested side effect.

A getter-backed namespace plus references to it can implement simple cases; a full module graph is needed for cyclic and asynchronous cases.

**LANGUAGE CHANGE:** yes; existing programs that observe snapshots, case folding, or reordered initialization change. Confidence: certain for snapshots; the other listed changes are explicitly stated in D303, not independently probed. Ordinary external ES-module imports are not shown defective by this probe.

### 5. BLOCKER — Plain finally and Effect finally have different failure algebras

**Location/rule.** Chapter 17, “Rules”; Chapter 15, “Regions inside a plain function”:

> “A failure during cleanup is never dropped.”

> “they compile to JavaScript's own statements”

> “Nothing inside can pause or be interrupted, so JavaScript's semantics match the machine's.”

**Position.** The last statement is false. JavaScript finally replaces a pending abrupt completion when cleanup throws. The Chapter 20 Final transition combines the original cause with cleanup failure. Neither suspension nor interruption is necessary to distinguish them. A defect is enough. E = never does not imply absence of defects.

**Confirmed.** [plain-finally/src/main.vibe](probes/plain-finally/src/main.vibe) throws a TypeError reading null.original and then a second reading null.cleanup in finally. Its Exit contains one Die, and Cause.pretty reports only cleanup. Both failures should remain under Chapter 17's rule. The cast in this probe is used only to trigger ordinary defects; Chapter 15 explicitly uses the same kind of defect to justify cold wrappers.

**Prior art.** ECMAScript [TryStatement evaluation](https://tc39.es/ecma262/multipage/ecmascript-language-statements-and-declarations.html#sec-try-statement-runtime-semantics-evaluation) selects a cleanup's abrupt completion. Effect's onExit frames use a different combination rule. Calling both rules “the same” conceals a language distinction.

**Exact replacement rule.**

> Every VibeLang finally, including one in an eligible plain function, preserves the pending completion. Cleanup runs once. Normal cleanup preserves that completion; failing cleanup combines with a pending failure using the same Cause normalization as framed execution, and fails a previously successful completion. Native JavaScript finally may be emitted only when equivalence with that rule is established. Otherwise retain frames or use a synchronous completion-and-cause helper. Hatches retain JavaScript finally.

Keep EK2006, which correctly forbids return/break/continue from replacing an exit, but cover throwing finalizers as well.

**LANGUAGE CHANGE:** yes for the Chapter 15 native rule; aligns it with Chapter 17. Confidence: certain.

### 6. BLOCKER — using explicitly permits two releases of one resource

**Location/rule.** Chapter 6, “using”:

> “A Disposable result also runs [Symbol.dispose]() at block exit. If its Effect release already disposes it, this disposes it twice (D94).”

Chapter 21 simultaneously states:

> “A value that needs release ... is owned by exactly one party at every instant”

**Position.** The spec knows the failure and standardizes it. Combining scoped Effect acquisition with a Disposable result must not register a second independent disposal obligation for the same resource. This is neither JavaScript resource management nor Effect's acquire/release ownership.

**Confirmed.** [disposal/src/main.vibe](probes/disposal/src/main.vibe) acquires a Disposable through Effect.acquireRelease, whose release calls Symbol.dispose. A single using prints ["dispose","dispose"]. Exactly-once release is false for this documented, accepted form. The workaround of wrapping the value in a holder should not be the default ownership law.

**Prior art.** ECMAScript resource management registers a disposal obligation for the using declaration; Effect registers one in acquireRelease. A language integrating them must define how obligations compose, not execute both and make every author audit idempotence. [OCaml's continuation/resource discussion](https://ocaml.org/manual/5.3/effects.html) illustrates why control and linear resources require a single ownership discipline.

**Exact replacement rule.**

> For an Effect acquisition, using supplies and closes the block Scope; the acquisition is responsible for registering release, and using does not additionally inspect or invoke a disposal method on its result. For a plain Disposable or AsyncDisposable initializer, using registers exactly one disposal operation. To acquire an unregistered Disposable through an Effect, use an explicit adapter that registers that disposal with acquireRelease. No implicit disposal is added to a scoped acquisition.

This uses rules the runtime can enforce without guessing whether some unrelated finalizer owns the returned value.

**LANGUAGE CHANGE:** yes; removes D94's double-disposal behavior. Confidence: certain.

### 7. MAJOR — No general hygiene law; the parser captures source bindings

**Location/rule.** Chapter 26, “Regions compile to frames”; Chapter 29, D104/D123; Chapter 28, “Linting”:

> “Region bodies are closures over the function's variables”

> “Names the parser writes for the checker are marked synthesized and kept out of scope analysis”

D123 promises free aliases for declaration imports, but nowhere establishes a binding-preservation law for every generated identifier and intrinsic.

**Position.** This is a missing compiler obligation in the spec, not a language rule authorizing capture. The observed capture also violates the advertised TypeScript scoping model. “Synthesized” is an AST flag, not hygiene. Lowering must preserve the binding graph, including generated references back to source bindings. A naming convention cannot reserve a legal identifier retroactively.

**Confirmed.** [parser-hygiene/src/main.vibe](probes/parser-hygiene/src/main.vibe) binds const $match1 = 99 and evaluates match (1) { when 1: $match1; default: 0; }. It compiles and prints 1. The generated match closure inserts const $match1 = 1, capturing the arm's source reference. Correct result: 99. The emitted JavaScript is retained in that probe's dist/main.js.

**Prior art.** [Scheme R6RS hygienic macro expansion](https://r6rs.org/final/html/r6rs/r6rs-Z-H-14.html#node_sec_11.19) distinguishes introduced bindings and binding identities. This obligation applies just as strongly to compiler-generated source as to macros.

**Exact replacement rule.**

> Every desugaring preserves source binding identity. Introduced bindings are fresh with respect to all source and generated bindings in every scope they can affect. References copied from source continue to resolve to their original bindings. Runtime intrinsics and compiler-owned types refer to private resolved symbols and cannot be shadowed by user declarations. No otherwise legal source identifier is reserved merely because a compiler emits it.

Apply this to match/is temporaries and labels, handle continuations, caught values, service/error/schema helpers, generated type parameters, $direct entries, import aliases, declarations, block completions, and nested TypeScript modules.

**LANGUAGE CHANGE:** no for capture avoidance; it makes the intended lexical rules explicit and corrects invalid lowering. Any deliberate user-shadowing of generated intrinsics must cease. Confidence: certain. A separate probe named generated-hygiene, using a local runtime binding, passed because that import alias was renamed correctly; the failure is not universal.

### 8. MAJOR — JavaScript lexical context is promised only in fragments

**Location/rule.** Chapter 13, “Evaluation order”; Chapter 26, function and region lowering; Chapter 29 D92/D104; Appendix C1:

> “A receiver is evaluated once and keeps its this.”

> “Region bodies are closures over the function's variables”

> “this keeps its JavaScript meaning”

**Position.** These cover some method calls and ordinary captured variables. They do not specify the lexical and activation-level obligations for every introduced function: arguments, new.target, super's home object and receiver, named-function-expression self-binding, arrows versus ordinary functions, or parameters and private environments. A continuation-frame invariant says where state lives; it does not say which source activation owns that state.

**Evidence and limits.** The current build passes [lexical-arguments](probes/lexical-arguments/src/main.vibe), preserving arguments[0] = 42 across a sleep and try/finally, and [lexical-super](probes/lexical-super/src/main.vibe), preserving a super call in an effectful child method. These are positive results. DECISIONS.md's “Known gaps” records older arguments/super failures; it does not establish that those failures remain in this build. No untested lexical-context failure is presented as confirmed.

**Prior art.** ECMAScript [arrow-function evaluation](https://tc39.es/ecma262/multipage/ecmascript-language-functions-and-classes.html#sec-arrow-function-definitions-runtime-semantics-evaluation) distinguishes lexical this/arguments/new.target/super from an ordinary function's environment. A generator replacement is not an arrow and does not inherit these properties automatically.

**Exact replacement rule.**

> Every source this, arguments, new.target, super reference, private-name reference, and named-function-expression self-reference retains the source environment and receiver that ECMAScript assigns it, except for an explicitly documented VibeLang construct. Generated function bodies introduce no source-visible activation or home object. A source arrow retains lexical bindings; a source ordinary function retains its own activation bindings. Parameter bindings, reassignment, defaults, recursion, extraction of methods, and suspension do not alter these associations. The rule applies to all wrappers, regions, matches, handlers, producers, hatches, and optimized variants.

Specify whether ordinary VibeLang functions are constructible; do not let the selected backend decide.

**LANGUAGE CHANGE:** no for promised JavaScript meaning; a new explicit constructibility restriction would be a language change. Confidence: high about the normative gap.

### 9. MAJOR — The evaluation-order paragraph is good but not a phase specification

**Location/rule.** Chapter 13, “Evaluation order” and program initializers; Chapter 20, “Objects”; Chapter 5, factories:

> “Arguments are evaluated left to right, each once.”

> “Only the initializer is held; calls in its operands keep their ordinary positions.”

> “A cold, reusable description of a computation. Constructing it runs nothing.”

> “The factory body runs as plain JavaScript at the call”

**Position.** “Once” must name an execution phase. A by-name argument runs zero, one, or many times; a held factory call constructs once; a cold exported wrapper defers its body; a factory may run getters and mutation while constructing that program. There is no universal theorem that every Effect value is side-effect-free to construct or that rerunning it repeats all work. Imported factories and memoizing Effects make that theorem false.

The specified parts are useful: strict operands follow JavaScript order; by-name calls reevaluate per run; factory snapshots can be held; method references keep receivers; a match subject is read once; layers are built per provide; producer bodies start on iteration. The remaining gaps are defaults/destructuring/rest binding; when a reusable callee or receiver is selected; enumeration and iterator closing while converting runtime collections; and repeated or nested program-topic uses. Ch. 5 rejects a pipe that mixes value/program topics but does not state a complete multiplicity/binding law when a program topic occurs twice.

**Measured implementation choice.** [parameter-phases](probes/parameter-phases/src/main.vibe), driven from [driver.ts](probes/parameter-phases/src/driver.ts), exports sample(x = ++state.defaults) with a mutable counter in its body. Immediately after sample(), both counters are 0. Two runs of the same Effect return 1 and 2 and increment both counters twice. Default initialization is per run in this case. That is a reasonable choice; it needs a normative rule.

**Prior art.** ECMAScript separates [function instantiation and parameter binding](https://tc39.es/ecma262/multipage/ordinary-and-exotic-objects-behaviours.html#sec-functiondeclarationinstantiation) from call-reference evaluation. Call-by-name additionally needs an explicit thunk/environment rule.

**Exact replacement rule for the current design, pending Finding 2.**

> Each expression is assigned a construction phase and an execution phase before lowering. A strict call captures its receiver, callable value, and actual argument values in source order at construction. A cold computation binds its formal parameters, including defaults and destructuring, afresh on each run, then executes its body. A factory binds formals and executes its factory body once per construction; only its returned program is rerunnable. A by-name position captures lexical binding locations, not their current values, and evaluates the entire argument expression separately for every requested run. A held initializer performs one construction and retains that program. Collection conversion is cold: construction captures the collection value; each run obtains an iterator or enumerates its record fields once in the declared order, converts the elements, and closes the iterator on abrupt exit. A single-use iterator retains its own state; rerunnability of an Effect does not make that iterator restartable. A program-topic occurrence denotes the same cold program value; each execution of it reevaluates the left expression.

Add separate rules for iterator failure/closing and prohibit ambiguous forms rather than extending “operands” by example.

**LANGUAGE CHANGE:** resolving previously unspecified cases can change existing behavior; the measured default-binding case already follows the proposed rule. Memoization and captured shared state remain observable and must be documented. Confidence: high.

### 10. MAJOR — Open error families make “exhaustive catch” a false general promise

**Location/rule.** Chapter 3, “Catching”; Chapter 29 D209/D218; DECISIONS.md D278/D304:

> “A match without default must handle every failure the try block can raise”

> “other types throw the proposal's TypeError”

> “An abstract error ... has the tag type string”

**Position.** An open class family is not a closed discriminated union. Listing known subclasses is not an exhaustive match on the base type. The current rules admit a partial handler and then turn a legitimate expected failure into a defect at the no-match helper. That is a valid partial-match feature if stated explicitly, but it contradicts the unrestricted catch promise.

**Confirmed.** [open-error](probes/open-error/src/main.vibe) declares abstract error Family, Known and Later subclasses, and matches a Family using only Known. It compiles without an exhaustiveness diagnostic; passing new Later() dies with TypeError: No match arm matched Later. The known subclasses are in the same file; this is not a package-loading accident.

**Prior art.** [Kotlin's exhaustive when](https://kotlinlang.org/spec/expressions.html#exhaustive-when-expressions) relies on sealed subtypes. [Rust match rules](https://doc.rust-lang.org/reference/expressions/match-expr.html) check a defined constructor space, not an open-world list of classes. TypeScript's [never-based exhaustiveness](https://www.typescriptlang.org/docs/handbook/2/narrowing.html#exhaustiveness-checking) is useful only if the narrowing predicate reflects the runtime test.

**Exact replacement rule.**

> A total match must establish that the unmatched value space is empty. A finite tagged union or data declaration supplies a closed constructor space. An open class/error family is not closed by the subclasses currently visible in the program; require a base-family arm or default. A catch match without a default must be total over E; otherwise it is a compile-time error. Partial matching, if retained, uses an explicit form and states that no match raises a defect. Runtime class/custom-matcher tests remain necessary where static structural typing cannot prove the test succeeds.

Retain D294's later correction that class/custom-matcher arms require a runtime assertion; do not restore its superseded assumption that shape implies instanceof.

**LANGUAGE CHANGE:** yes for currently accepted partial matches on open families. Confidence: certain.

### 11. MAJOR — Callback polymorphism depends on whether a type alias was extracted

**Location/rule.** Chapter 16, first section:

> “only a function type written in place gains a contract, so a named one keeps TypeScript's meaning and takes plain functions.”

**Position.** The text supplies a rule, but the rule breaks abstraction. Replacing f: (a: A) => B with a name for that same function type changes whether the callee can pause, whether errors and services are propagated, and the emitted callback ABI. Alias expansion should not choose application semantics. The same problem occurs when a function-or-Effect destination selects a representation from the callback's parameter count.

**Prior art.** [Koka's polymorphic map](https://koka-lang.github.io/koka/doc/book.html#sec-polymorphic-effects) exposes the callback's effect row in the function type. A row parameter is part of the signature, not a property of its typography. TypeScript aliases ordinarily denote their target types.

**Exact replacement rule.**

> Callback effect polymorphism is expressed in the canonical function type after alias expansion. A callback with result B!E!R carries explicit or quantified E and R independent of where its type is written. A plain JavaScript callback type remains plain in every position. If implicit row-parameter sugar is retained, it applies equally to an inline type and an alias with the same canonical type, and its expansion is specified before checking or emitting declarations. Parameter count never selects function versus program representation.

**LANGUAGE CHANGE:** yes; effect-polymorphic callback types and plain callback types must be written distinctly or canonically expanded. Confidence: certain about the current typography-dependent rule; no runtime failure is claimed here.


### 12. MAJOR — Separate-compilation safety relies on metadata the spec says is not emitted

**Location/rule.** Chapter 9, “Handlers and concurrency”; Chapter 27, “Declarations and metadata”:

> “their declarations carry the compiler's metadata, and the compiler checked their bodies when it built them.”

> “the compiler neither emits nor reads it”

The second quote specifically concerns control-class and $direct metadata. The document names no separate, implemented certificate that establishes the first quote's cross-package safety claim.

**Position.** A consumer must not infer “checked VibeLang body” from a declaration's shape. A foreign function can advertise the same Effect<A,E,R>, and a declaration cannot by itself prove fiber affinity, continuation non-escape, or absence of hidden forks. Likewise, an ordinary computation and a synchronous factory can have identical TypeScript signatures while differing at call time. .d.ts is an ABI promise, not a runtime proof.

**Prior art.** [TypeScript's compatibility documentation](https://www.typescriptlang.org/docs/handbook/type-compatibility.html#a-note-on-soundness) acknowledges structural typing's limits. A separate compiler's stronger effect-safety claims require a specified trusted interface. [OCaml 5 explicitly distinguishes its runtime handler support from static effect safety](https://ocaml.org/manual/5.3/effects.html); VibeLang must make its own stronger boundary precise.

**Exact replacement rule.**

> Declaration emit preserves A, E, R, generic callback rows, nominal service/control identity, the public callable convention, and explicit factory staging. Any safety fact a consumer uses to relax a foreign-code restriction is represented in a versioned compiler metadata contract and is validated by that consumer. Absent or unsupported metadata means foreign code and receives the conservative foreign-code checks. Private direct-call metadata can affect performance only. The same source compiled separately and together has identical public behavior.

Add declaration round trips through stock TypeScript and a VibeLang consumer, including live re-exports, defaults, factory timing, producers with control requirements, and aliased imports. The ordinary sample declaration in parameter-phases correctly advertises an Effect-returning function; that positive result does not settle these stronger cases.

**LANGUAGE CHANGE:** rejecting unverified library cases can affect existing programs; correctly emitted APIs do not change. Confidence: high about the incompatible promises; no untested package exploit is claimed.

### 13. MAJOR — Data methods and same-named exports turn declaration accidents into language APIs

**Location/rule.** Chapter 13, “Methods on Effect's data types”; Chapter 1's same-named-export rule; Chapter 29 D295/D311:

> “in effect/dist/<Module>.d.ts”

> “whose first parameter is named self”

> “The module's exports win.”

**Position.** A parameter's label and a package's declaration-file layout are not semantic properties of a function. Renaming self to source can remove a method without changing any TypeScript function type. D295's exception table confirms this is an implementation heuristic elevated into a rule. The D311 precedence rule adds another dependency on package evolution: adding a module export join can redirect a formerly service-backed Module.join call and alter R while leaving the source call spelling intact.

A same-named export is a defensible namespace convenience if it is symbol-based and stable. It is not a license to inspect the text “Experimental”, “FileSystem”, or an import alias during lowering. D313's Experimental namespace needs the same resolution rules as any other import.

**Prior art.** The [TypeScript handbook's function types](https://www.typescriptlang.org/docs/handbook/2/functions.html) give parameter names a descriptive role. ECMAScript member access selects a particular reference; it does not infer extension methods from filenames or parameter names.

**Exact replacement rule.**

> Extension methods are declared in explicit adapter metadata keyed by resolved module and function symbols and a designated receiver parameter position. Parameter names and filesystem paths have no semantic role. A namespace's designated service/type export is likewise recorded by resolved export identity and follows import aliases. A module export and a synthesized service/extension member of the same surface name produce an ambiguity diagnostic requiring an explicit qualified reference; adding an export never silently redirects an existing synthesized call.

**LANGUAGE CHANGE:** yes for parameter-name recognition and winning collisions. Confidence: certain about the published dispatch rules.

### 14. MAJOR — Trust and effect-safety claims need an explicit trusted computing base

**Location/rule.** Chapter 10, “Code that is not Effect”; Chapter 15, “The rule”; Chapter 16, fiber behavior:

> “and the functions and values it returns”

> “Calls of TypeScript code ... are ordinary calls needing no trust boundary”

> “the compiler assumes the argument may run on another fiber.”

**Position.** Several boundaries are promises by convention: TypeScript's declared E/R, JSDoc @throws, every @effect/* export, values returned by those exports, plain-annotated wrappers, any/assertions, and the fiber-behavior table. They are not body-verified effect contracts. In particular, a package's returning a supplied function does not establish the function's provenance or purity, and no ordinary function type certifies that a JavaScript library will invoke it only on the expected fiber.

These limits do not make the typed-error channel useless. E should be a sound over-approximation of escaping Fail values in the verified subset; arbitrary defects are intentionally outside E. “Cannot fail” must mean no expected failure, not totality, absence of JavaScript exceptions, or purity. Blanket trust must not be presented as compiler proof of those stronger properties.

**Prior art.** [TypeScript's documented soundness tradeoffs](https://www.typescriptlang.org/docs/handbook/type-compatibility.html#a-note-on-soundness) are not automatically acceptable for additional VibeLang guarantees. Koka separates a function's effect row from the identity of the module returning it.

**Exact replacement rule.**

> The effect-safety guarantee applies to checked VibeLang bodies and declared, trusted boundary adapters. Foreign declarations, assertions, any, unchecked callback protocols, and trusted implementation metadata are explicit assumptions of that guarantee. Trust attaches to the resolved callable adapter, not transitively to arbitrary values returned by trusted code. A plain return annotation introduces no additional trust. Native APIs that invoke user code implicitly, including serialization and coercion protocols, must declare their callback convention or require a JavaScript hatch. A missing fiber-behavior declaration receives the conservative cross-fiber rule.

Specify E/R inclusion for every primitive and adapter, including a mapper that itself fails. State that Scope in R tracks a release obligation, not a Rust-style proof that a resource value cannot escape and later be used after closing.

**LANGUAGE CHANGE:** yes where blanket trust or a plain annotation currently bypasses boundaries. Documenting existing trusted assumptions alone changes no behavior. Confidence: high about the stated assumptions; this finding does not claim every trusted function is wrong.

### 15. MAJOR — The finalization promise excludes an acknowledged Effect boundary, but the chapters hide the exception

**Location/rule.** Chapter 17, “Rules”; Chapter 7, concurrency; Appendix A F11; DECISIONS.md D256:

> “A failure during cleanup is never dropped.”

> “timeout still drops a loser's cleanup failure (D305, D256)”

> “This does not extend to failures an Effect operator discards by design”

**Position.** D256 is a reasonable compatibility boundary, but it must be in the normative failure chapter. As written, a reader can derive an absolute preservation law and then lose a cleanup defect through timeout/race. The issue is the scope of the guarantee; VibeLang need not fork Effect's race implementation to fix the document.

The opposite mistake is also possible: treating every mixed cause as uncatchable. D305/D306 and the measured Effect 4.0.6 source distinguish them. A Die prevents typed recovery; a Fail beside Interrupt can be recovered, dropping the interruption and later failures. Pending fiber interruption can still bypass recovery frames. Those are different states.

**Source check.** The probe-linked installed package reports effect 4.0.6. Its internal/effect.ts causeElectDefects/findRecoverableError, lines 178–199, and catch_, lines 2708–2722, implement defect precedence and recovery beside interrupts. This agrees with Chapter 17, and contradicts Chapter 3's sentence claiming Effect.catch would drop the crash. [Effect's pinned source](https://github.com/Effect-TS/effect/blob/effect%404.0.6/packages/effect/src/internal/effect.ts) is the relevant primary reference, rather than Effect 3's differently shaped Cause API.

**Exact replacement rule.**

> VibeLang-owned finalization combines cleanup failures with the current completion before reporting that completion. Every owned finalizer runs once in reverse registration order under the specified mask. This local preservation guarantee ends when the resulting Exit is passed to an Effect operator whose documented policy discards that Exit; timeout and race may discard loser-cleanup reasons, as D256 records. On Effect 4.0.6, typed catch recovers the first Fail only when no Die or abandonment prevents it; recovery discards other recoverable reasons as Effect.catch does. A pending interruption and an Interrupt reason in an already completed Cause are specified separately.

Also define ordinary throw as Fail(value) and give Cause rethrow an explicit typing/elaboration rule, including unions and generic/unknown operands; “throw with a Cause” currently leaves the classification mechanism unstated.

**LANGUAGE CHANGE:** no for documenting D256 and the pinned mixed-cause rules; a new explicit Cause-rethrow form would be a language change. Confidence: certain about the textual contradiction; timeout was not independently re-probed in this review.

### 16. MAJOR — “No new type errors” is not a semantics-preservation criterion for rewrites

**Location/rule.** Chapter 28, “Diagnostics”; DECISIONS.md D291, D288–D290:

> “wherever the VibeLang form keeps the program's meaning”

> “it writes a file only when the fixed program reports no error the original did not”

**Position.** The second condition is useful validation, but cannot discharge the first. Two well-typed programs may differ in value, call count, binding, failure classification, scheduling, service identity, or resource lifetime. The spec itself supplies witnesses: the captured match binding, snapshot exports, and annotation-selected factory staging all type-check while changing observations.

The log also records a real-world D288 correction where deleting Effect.succeed changed a callback's emitted form while remaining type-correct. D289 still describes a mixed-cause difference between source catch and Effect combinators that D305/D306 now remove. A rewrite cannot use both historical descriptions as its contract.

**Prior art.** Compiler correctness is observational equivalence under the language's specified observations. Type preservation is necessary for a typed rewrite, but it is a different property.

**Exact replacement rule.**

> Every automatic rewrite has a stated semantic precondition and preserves success values, evaluated bindings, evaluation order/count/phase, expected failures and defects, service lookup, resource lifetime, and the language's permitted interruption/scheduling observations. The absence of new diagnostics is an additional check, not evidence of equivalence. Where equivalence is not established, present a migration with its behavior change and require an explicit selection; do not include it in automatic safe fixes.

For optimizations, make Chapter 30's G10 differential check an acceptance gate against an unoptimized semantics. Preserve once-only callee/member references and all lexical environments through that comparison. An explicit completion/reference IR would make the obligation reviewable; an IR is an implementation recommendation, not a prerequisite for language validity.

**LANGUAGE CHANGE:** no for fixes advertised as behavior-preserving; some offered fixes must be withdrawn or reclassified. Confidence: certain about the inadequate criterion.

### 17. MINOR — There is no single current normative document

**Location/rule.** Introduction, “Status”; Chapter 29 conclusion; Chapter 30 opening:

> “Every rule in this specification is decided.”

> “No language or repository decision remains open here.”

**Position.** The document is simultaneously a language definition, an experiment log, a compiler status report, and a transcript of superseded decisions. Its precedence rules are insufficient to determine the current language.

Concrete discrepancies found by reading all chapters:

- Chapter 3 says Effect.catch drops a crash beside an expected failure; Chapter 17 says Effect 4.0.6 preserves the whole defect-bearing cause without typed recovery.
- Chapter 12's pattern-matching answer and Appendix B's TC39 table say match is not used; Chapters 3 and 11 specify match, is, and data patterns. The same appendix says throw expressions are not adopted while Chapter 3 adopts them.
- Chapter 29 contains seven identical D13 rows, including six consecutive rows after D129, instead of a complete current decision sequence. Its introductory numbering stops at D124 while later rows reach D312.
- D278/D279/D283/D303/D304 contain substantial error-class, schema-error-family, module, and mutable-export behavior that is absent from the corresponding explanatory chapters; diagnostics mentioning them do not specify them.
- D249 changes trust to a value-level API for the text projector; Chapter 10 still teaches JSDoc as the main contract, and the inventory is needed to discover which compiler path owns which rule.
- D294's final-arm optimization and its important subsequent class-pattern correction have no clear normative presentation in the matching chapter.
- D310–D313 are called provisional in the log and await the owner's review, while the introduction and Chapter 30 deny open design questions.
- Some fences labelled dts use VibeLang contract shorthand although Chapters 14 and 27 promise ordinary TypeScript declaration syntax. Rendered shorthand must be labelled as presentation, not purported declaration output.

**Prior art.** A normative specification separates syntax, static semantics, dynamic semantics, and conformance requirements from non-normative rationale and implementation status. ECMAScript's abstract operations have a different role from engine notes or test counts.

**Exact replacement rule.**

> Chapters 13–17 and a new source elaboration appendix are the sole normative source-language rules; Chapter 20 is the normative runtime model. Each feature links to one current rule. Examples, decision history, measurements, implementation coverage, and proposed changes are non-normative. A new decision changes the language only when its normative rule and all conflicting examples are updated. Provisional decisions are explicitly outside the current language until accepted.

**LANGUAGE CHANGE:** no, except where reconciling contradictory behavior requires an owner decision. Confidence: certain.

## Evaluation, types, and boundary obligations at a glance

These are the specific unresolved obligations behind the findings, rather than a claim that evaluation order is wholly absent.

| Area | Specified adequately | Missing, inconsistent, or dependent on convention |
| --- | --- | --- |
| Strict expressions | Ch. 13: left-to-right arguments, once-only receiver/getters, short-circuit example; Ch. 27: operands retain order | A complete Reference/GetValue rule for callees, computed accesses and assignments across pauses; lexical environments through every introduced function |
| By-name calls | Entire expression reruns; lexical locals fresh per execution | Explicit phase/multiplicity rules for duplicated topics and general collection conversion; annotations also select a different holding strategy |
| Coldness | Exported ordinary computation wrappers defer body work; direct variants cannot eagerly construct success values | Effect values can encapsulate shared/memoized state; factory construction is eager; no universal purity or repeatability guarantee follows from the Effect type |
| Function entry | Default/constructor/accessor bodies cannot run programs; factory body must remain plain | Default/destructuring/rest initialization phase and activation identity across repeated runs are not stated as a general law |
| Services and layers | Unique derived keys, nominal R, member requirements, build-time capture versus call-time lookup, residual requirements, layer ownership, duplicate/cycle checks | Metadata and runtime-declaration agreement at package boundaries; default-service and experimental dual-provider identities need canonical symbol rules |
| Failure algebra | Ch. 17/20 define Fail/Die/Interrupt/abandonment, mask finalizers, LIFO cleanup, and no jumps from finally | Plain finally contradicts framed combination; D256's discarded-loser boundary is missing from the main promise; Cause-valued throw classification needs an explicit rule |
| Match/data | Once-only subject; data variants are closed tagged unions; D307 uses Effect's constructors; class patterns use instance identity | Open families need an explicit totality rule; D294's current runtime-assertion policy is buried in the log; generated names are unhygienic |
| Type inference | Written E/R are upper bounds; complete contracts contribute their declared width; recursive SCC inference has an annotation escape | Sound handler answer types; canonical callback rows; precise trusted subset and verification of cross-package facts |
| TypeScript boundary | Ordinary exported computation returns Effect; producers expose Stream; eligible plain annotations retain plain ABI; services emit interfaces and keys | Factory staging in the ABI, certified metadata, inline module live bindings/initialization, and clear differences between normal imports and the inline escape |
| Iteration/concurrency | Sequential ordinary calls; explicit concurrent forms; block-owned forks; cleanup ordering; conservative cross-fiber table | Producer-to-Stream adaptation changes fiber identity and therefore handler reachability; that effect must be checked at adaptation, not merely at a later named combinator |
| Scope safety | using supplies a block Scope; acquisitions without using remain caller-owned | Scope typing does not prohibit returning a closed handle; returning a block-owned fiber is expressly allowed even though it is already interrupted; these are limits, not ownership proofs |

An Effect is a reusable description in the sense that its representation can be run again. It is not a referentially transparent recipe, and re-running it need not recreate captured resources, undo mutation, or rerun a factory. The spec should use “fresh activation per run” where that is what it proves.

The phase rule must also distinguish capturing a binding location from capturing a value. A thunk containing object.method(arg) can select a new object or method on each run; a strict call whose resulting Effect is retained must not silently reselect its callable each time. That distinction matters for mutable bindings, getters, and import live bindings even without concurrency.

## What the spec gets right

- **A meaningful runtime invariant.** Chapter 26's frame invariant explains why every pause/capture must have its continuation state on heap frames and why source finally cannot remain in a generator. This directly prevents an entire class of control and cleanup bugs.
- **One-shot ownership is explicit.** Chapters 20–23 specify deep handlers, clause context, same-fiber consumption, owner-driven abandonment, sticky pending interruption, and deterministic cleanup. [OCaml 5's continuation discipline](https://ocaml.org/manual/5.3/effects.html) is relevant prior art; VibeLang's explicit owners make its intended resource policy unusually clear.
- **The typed-error/defect distinction has a real pinned model.** Chapter 17's updated D305/D306 rules agree with the inspected Effect 4.0.6 source. They distinguish an interruption reason from pending interruption and avoid pretending that E = never means a body cannot crash.
- **Source order and cold wrappers are stated, not merely illustrated.** Chapters 13 and 15 explicitly forbid reordering, duplication, eager body work, and removing suspension points as optimization. The morning's compiler bugs in these areas violate existing requirements.
- **Dependency injection is genuinely designed.** Chapter 4 addresses nominal keys, separate acquisition and method requirements, per-call provider lookup versus captured implementations, residual graph inputs, duplicate providers, cycles, and release after failed builds.
- **The limitations of the runtime backend are admitted.** Chapters 22 and 25 identify snapshot Context, non-delimited AsyncLocalStorage, private Effect dependencies, and the reference-machine disagreement. Those are more useful than an unsupported claim that passing two unrelated test suites proves equivalence.
- **Several suspected implementation failures did not reproduce.** The arguments, super, and generated-runtime-import probes passed. A rigorous review must retain those results as evidence against overgeneralization.

## Probe record and confidence

Each directory contains src/main.vibe, the probe harness's configuration and links, generated dist output when compilation succeeded, and result.log. The harness emitted a warning that its optional @effect directory was absent; none of these probes required an @effect package. They used the installed effect 4.0.6 and vibelang-runtime. Probes ran sequentially with a 25-second bound. Compilation success is reported separately from runtime success.

| Probe | Observation | Classification |
| --- | --- | --- |
| handler-answer | EK2119 warning, compile 0; TypeError at n.toFixed, runtime 1 | Confirmed type-preservation failure permitted by spec |
| parser-hygiene | Source asks for outer 99; runtime prints 1 | Confirmed capture from missing hygiene requirement |
| shadow-pattern | Local Option.Some becomes isSome lookup; TS2551 | Confirmed deliberate spelling semantics |
| shadow-runner | Compile/runtime 0; main does not run; entry absent | Confirmed spelling-based entry suppression |
| module-live | [0,0] after bump; ordinary module behavior is [0,1] | Confirmed snapshot rule |
| plain-finally | Only cleanup TypeError remains; one Die | Confirmed native/framed-finally contradiction |
| disposal | ["dispose","dispose"] from one using | Confirmed explicitly allowed double release |
| type-directed-run | Same Exit object returned under two declarations becomes Exit data versus 42 | Confirmed intended type-directed execution |
| open-error | Compile 0; valid Later instance causes no-match TypeError | Confirmed open-family exhaustiveness limitation |
| parameter-phases | Call: counters 0/0; runs return 1,2 with counters 1/1,2/2 | Measured staging choice; no violation asserted |
| lexical-arguments | arguments[0] stays 42 across pause and region | Pass |
| lexical-super | Effectful child method's super.value() returns 42 | Pass |
| generated-hygiene | Local runtime value survives generated import aliasing | Pass; parser hygiene still fails independently |

Confidence is **certain** for quoted deliberate rules and the listed observations, **high** for the identified normative omissions and contradictions. Proposed minimal-call semantics is a design judgment with explicit migrations, not an empirical claim of having proved a replacement compiler correct.

## Reading list: the three changes that would remove the most compiler bugs

1. **Replace Chapter 13's context-selected execution with strict calls and explicit programs.** Start with the value/computation distinction in [Eff's operational and typing rules](https://www.eff-lang.org/handlers-tutorial.pdf), then preserve direct-style function application as in [Koka](https://koka-lang.github.io/koka/doc/book.html). Delete implicit quotation, arbitrary Effect-result unwrapping, and typography-selected callback ABIs. This removes the largest multiplication of lowering cases.
2. **Add a binding-and-evaluation preservation appendix before extending syntax.** Model source References, environments, and completions using [ECMAScript EvaluateCall](https://tc39.es/ecma262/multipage/ecmascript-language-expressions.html#sec-evaluatecall), [function environments](https://tc39.es/ecma262/multipage/executable-code-and-execution-contexts.html#sec-function-environment-records), and [Scheme hygiene](https://r6rs.org/final/html/r6rs/r6rs-Z-H-14.html#node_sec_11.19). Require alpha-renaming invariance and optimized/unoptimized observational comparisons, including receiver/getter/argument order, short circuits, lexical context, import updates, and finalization.
3. **Close the type-and-exit contracts instead of documenting unsafe approximations.** Make handler answer types sound or require annotations; give total matching a closed constructor space using [Kotlin sealed exhaustiveness](https://kotlinlang.org/spec/expressions.html#exhaustive-when-expressions) and [Rust matching](https://doc.rust-lang.org/reference/expressions/match-expr.html); write one current failure/ownership law matching [Effect 4.0.6](https://github.com/Effect-TS/effect/blob/effect%404.0.6/packages/effect/src/internal/effect.ts), with explicit FFI and discarded-loser boundaries. Apply it to native and framed code, then make .d.ts and metadata carry exactly the promises consumers are allowed to use.