Summary

Audit during PR #650 surfaced ~10 spec sites where the documented language behaviour is in tension with the stated design principles in §0.2 ("Explicitness") and §0.2.3 / §0.3.2 ("One canonical form / no shorthand / no implicit conversions / no default arguments").

Each item is individually defensible as a deliberate ergonomic tradeoff, but the principles as currently written claim absoluteness ("There is no implicit behaviour for the model to infer or hallucinate") that the spec then partly contradicts in later chapters. The result is a spec that's internally inconsistent on its own foundational rules.

Drift inventory

Proposed resolution shape

Two options, not mutually exclusive:

Option 1 — Strengthen §0.3 to enumerate the deliberate implicit surfaces

Add a §0.3.6 or similar:

Implicit surfaces excluded from §0.2.2 — the following are deliberate exceptions where the cost of explicitness outweighs the principle benefit:

1. The standard prelude (§9.1.2) — Option, Result, Ordering, UrlParts, and their associated combinator and accessor functions are available without declaration.
2. The IO effect (§7.5) — operations are available when effects(<IO>) is declared, without a user-side effect IO { ... } declaration.
3. The resume continuation (§7.5) — implicitly bound inside handler arms.
4. Ability auto-derivation (§9.X) — built-in abilities (Eq, Ord, Hash, Show) are derived automatically for ADTs whose fields support them.
5. Primitive-to-String coercion inside InterpolatedString (§1.7) — primitive types (Int, Nat, Bool, Byte, Float64) are wrapped via *_to_string automatically; the interpolation syntax \(...) is the explicit marker.
6. effects(pure) default on function-type annotations (§2.5) — type-level annotation only; function declarations still require an explicit effects(...) clause.
7. Verifier-mediated subtyping (§2.2.1) — Int <: Nat is accepted at type-check time but the verifier discharges an obligation; the conversion is syntactically silent but semantically verified.
8. State<T>.get() Unit-arg elision (§9.X) — single built-in exception.

This makes the principle honest. The cost is acknowledging the design has 8 narrowly-scoped exceptions; the benefit is that the spec no longer contradicts itself.

Option 2 — Triage each item separately

Some of the "exceptions" above may not be defensible on inspection:

• D (multiple requires equivalence) — the "one canonical form" violation here is real. The justification ("more precise error reporting") could instead be solved by a different mechanism (e.g., named requires clauses) without two textual forms.
• E (@Fn<A,B>.0 shorthand) — needs investigation. If @Fn<A,B>.0 is the only way to refer to the function argument (and the word "shorthand" is misleading), §3.7 should be reworded. If there's an alternative long form, one of the two should be deprecated.
• J (optional module statement) — §10 grammar already marks visibility as parser-flexible-but-checker-mandatory. The module statement could do the same: parser accepts both forms, but a future linter/vera fmt could enforce one canonical shape.

Items where the implicit-ness is genuinely load-bearing (A, B, F, H, I, K) get enumerated in §0.3 via Option 1. Items where the implicit-ness is just unfixed legacy (D, E, J) get individual close-out PRs.

Recommendation

Both. Start with Option 1 (§0.3 enumeration) as one PR — honest framing, no behaviour change. Then file 3 follow-up issues for D, E, J as separate triage candidates.

Why this matters

LLMs reading the spec take §0.2.2 literally ("there is no implicit behaviour"). When the same model then writes a Vera program that depends on prelude Option or auto-derived Eq, it experiences a contradiction with the principle as it understood it. The honest framing reduces this confusion — "the language has X implicit surfaces, here they are, expect them" is better than an absolute claim that the rest of the spec quietly walks back.

Source

Audit performed 2026-05-11 during PR #650 review pass.

Related

• PR Small docs sweep: #557 + #561 + #560 + #607 + #608 + #512 #650 — addressed item K (the §2.2.1 Int↔Nat wording) by reframing "implicitly" → "syntactically silent but semantically verified". This is the model fix for how to discuss verifier-mediated subtyping; could be extended to other items.
• §0.2.2 — the principle being audited.
• §0.3.2 — the non-goal being audited.