§9. Open questions

Generated from docs/LANGUAGE.md §9. This is the normative specification; for a guided tour see the Language and Neurosymbolic sections.

• Q1 — Keyword user testing. simulate (physics connotation for robotics users) and the D8 monitor retention both need validation with the actual target population before 0.1 freezes; ported vs absorb likewise (12 open questions).
• Q2 — Graded truth beyond thresholds. Threshold-at-branch is decided (D2); whether a graded region with provenance-semiring propagation (Scallop, arXiv:2304.04812) earns its complexity is a theory-track question shared with THEORY.md.
• Q3 — Statistical gradual verification metatheory. No published soundness/blame theorems exist for a lattice with a statistical(α) point; candidate base Gradual C0 + conformal risk control (05 §6.10). This is Sema’s publishable PL contribution and its largest formal risk.
• Q4 — Conformal validity under feedback. Self-healing and degrade actions shift the distribution their own monitors calibrated on; only nascent 2026 literature touches this (05 §6.10, 10).
• Q5 — ~= calibration data. No published head-to-head of static-embedding vs small-transformer agreement on equality-style judgments (vs MTEB retrieval); the default judge’s threshold certificates need an in-house eval (06).
• Q6 — Mutation-score thresholds per assure grade. Google uses ~1 sampled mutant per covered line; the right green-gate threshold under compile-latency budgets is unset (09 open questions).
• Q7 — Constrained decoding beyond syntax. How far the GBNF/Earley artifact can extend into the type/contract layer for on-device generation of Sema is open research (12 §6; 04 §2.6).
• Q8 — Reasoning-degradation freshness. The format-restriction-hurts-reasoning result (arXiv:2408.02442) predates 2026 models; re-benchmark before hard-freezing simulate’s two-phase emission parameters (03 open questions).
• Q9 — Effect vocabulary cross-check. The LMPL/SPLASH 2025 algebraic-effects-for-LLMs paper could not be extracted; read it before freezing the §3.6 effect operation set (05 open questions).
• Q10 — Generators and yield. Resolved by D39 (§5.25). The deferral’s two objections are answered structurally: stream values are affine scoped resources, so no coroutine frame outlives its scope or escapes the journal’s view; pulls are data-ordered under structured concurrency, so effects journal in pull order and replay is deterministic. What remains open moved to Q16 (event-time semantics and distributed stream topology).
• Q11 — Module ABI and editions. §5.18 fixes surface and resolution; the stable module ABI (cross-edition linkage, pub contract hashing across compiler versions, lockfile interaction) is unspecified and gates any pre-compiled package registry.
• Q12 — Dynamic subscription and channels. event.subscribe is reserved and Channel[T] deliberately absent (§5.17/§5.19): plugin-style runtime subscription and point-to-point typed channels wait on evidence that static subscribers are insufficient, because both hide dataflow from the compiler.
• Q13 — Streaming structured decode. Partially resolved by D39: decode[Stream[U]] (§5.25) is the element-granular form — each element is validated and repaired independently as it completes, so consumers act on early elements before the tail exists. Still deferred: intra-element streaming — decoding a single struct field-by-field as tokens arrive (partial typed objects, repair mid-value) — because an invariant cannot be checked on a half-built value; contract atomicity holds at element granularity. Revisit when the owned-engine path (§5.5) is real.
• Q14 — Staging surface depth. §5.23 fixes Code[T], admission, and sandboxed interpretation; two extensions are deferred: (a) a quasiquote/splice surface for constructing staged code structurally instead of via text (hygiene, capture rules, and constrained-decoding interaction are unsettled), and (b) how much of the L1 gauntlet can run at runtime admission under an interactive budget — a budgeted property-check subset would raise staged code’s behavioral guarantee above best_effort without waiting for the full heal-grade gauntlet. Both gate on the tier-0 interpreter existing.
• Q15 — Service surface extensions. §5.24 fixes unary typed calls, and streaming methods are now resolved by D39 (§5.25: the wire rule, credit flow control, terminator law — a service method carrying a stream is the sanctioned cross-process streaming shape, as this entry anticipated). Still deferred: non-Sema peer schema import (OpenAPI/protobuf → derived struct+service declarations, likely a sema bind-api toolchain command rather than language surface), discovery/mesh integration, and whether event subscriptions should ever cross process boundaries (today: explicitly not — D29).
• Q16 — Stream semantics beyond point-to-point. §5.25 fixes one producer, one consumer, wall-clock pull order. Deferred until real workloads demand them: event-time semantics (watermarks, out-of-order elements, late-data policy — the Flink/Beam problem space); cross-stream joins and fan-in/fan-out topologies (today: compose services and events explicitly); and long-horizon replay retention for unbounded streams (digest journaling bounds space, but pinned-source replay of a live feed is only as durable as the source — a retention/compaction story is unwritten).
• Q17 — Debugging surface depth. §5.26 fixes markers, snapshots, taint-forking, and pipeline provenance. Deferred: live interactive stepping across service boundaries (correlation ids already stitch post-mortem traces; pausing two processes coherently is a distributed-snapshot problem); watch expressions that carry effects (today: only pure predicates and session-budgeted judges); and debug-taint granularity (whole-run today — per-scope tainting would let an edited subtree coexist with clean evidence elsewhere).
• Q18 — Secrets and masking depth. §5.27 fixes the two-tier model and default-on masking. Deferred: how deep Secret[T] goes (taint-propagation through derived values — does f"{token}" stay secret? — interacts with §3.5’s lattice and GOVERNANCE’s declassification story); per-sink disclosure-policy granularity (per-namespace, per-field, per-tenant?); the scrubber pattern set’s maintenance/versioning discipline; and log sampling strategies under rate budgets (head vs tail sampling changes what evidence survives — today: deterministic per-namespace budgets, drops journaled).
• Q19 — Symbolic mathematics depth. §5.28 is numeric-with-provenance by design. Deferred: a symbolic layer (CAS simplification, exact rationals, symbolic integration/differentiation with certified rewrite rules); quantifiers over unbounded domains via SMT discharge (∀/∃ as verification obligations rather than iteration — would join the §5.7 evidence engine); units/dimensional analysis on scalar types; and which further atlas kernels (spectra, FFT/transforms, sparse/structured matrices) earn native implementations — driven by the robotics/dynamics workloads.