The problem
The most dangerous semantic uncertainty failure mode is a tool/external call that returns a well-typed value whose semantic shape is never verified. No as cast, no escape hatch, fully typed — and quietly wrong.
// Typed as string. Assumes it's a valid URL. Compiler sees nothing wrong.
const endpoint = await config.get("webhook_url");
http.post(endpoint, payload); // UNS005: no contract on what config.get returns
Proposal
Introduce UNS005 — fired by the compiler (inferred, not programmer-applied) when an external/tool call has no declared output contract the compiler can verify.
"Declared output contract" means one of:
- The callee's return type is a primitive (
number, boolean, null) — structurally unambiguous
- The callee has an
ensures: "..." annotation (or the future intent:-style contract equivalent) on its header
- The call site wraps the result in a contract check (schema validation, exhaustive match on a discriminated union)
- The call site is inside
unsafe "<reason>" { } explicitly accepting the uncertainty
UNS005 is compiler-inferred (unlike UNS001-UNS004 which are triggered by programmer-applied unsafe blocks). This keeps the two layers distinct — a reviewer can tell at a glance whether the author made a deliberate choice or the compiler is flagging an omission.
Failure mode addressed
A tool call completes, the return is well-typed, the compiler sees nothing wrong — and the result is quietly incorrect in a way only the runtime context can detect.
This is the exact gap from issue #48, question 3 (missing false negatives). UNS005 fires where UNS004 currently cannot.
Scope
This is a follow-on to the ensures: / intent: axis. The mechanical vocabulary for output contracts needs to land first (or in parallel) — otherwise UNS005 fires on everything and becomes noise. Suggest gating UNS005 on ?bs 0.9 or later.
Related
The problem
The most dangerous semantic uncertainty failure mode is a tool/external call that returns a well-typed value whose semantic shape is never verified. No
ascast, no escape hatch, fully typed — and quietly wrong.// Typed as string. Assumes it's a valid URL. Compiler sees nothing wrong. const endpoint = await config.get("webhook_url"); http.post(endpoint, payload); // UNS005: no contract on what config.get returnsProposal
Introduce
UNS005— fired by the compiler (inferred, not programmer-applied) when an external/tool call has no declared output contract the compiler can verify."Declared output contract" means one of:
number,boolean,null) — structurally unambiguousensures: "..."annotation (or the futureintent:-style contract equivalent) on its headerunsafe "<reason>" { }explicitly accepting the uncertaintyUNS005is compiler-inferred (unlike UNS001-UNS004 which are triggered by programmer-appliedunsafeblocks). This keeps the two layers distinct — a reviewer can tell at a glance whether the author made a deliberate choice or the compiler is flagging an omission.Failure mode addressed
This is the exact gap from issue #48, question 3 (missing false negatives). UNS005 fires where UNS004 currently cannot.
Scope
This is a follow-on to the
ensures:/intent:axis. The mechanical vocabulary for output contracts needs to land first (or in parallel) — otherwise UNS005 fires on everything and becomes noise. Suggest gating UNS005 on?bs 0.9or later.Related
ensures:complement tointent: