What the linter can actually promise

Why bother being precise

The pitch is a mechanism a public-sector lawyer can inspect, test before signing, and replay in front of a judge. That pitch is only as strong as its weakest overstated claim: the first time an expert witness shows that “pool safety is verifiable” was a fragment-only property, the damage lands on the boring-and-honest brand rather than on a footnote.

Precision here is cheap. Every claim below stays true after correction - it just acquires a scope.

The claims, sorted

Claim	Actually	Cost
Determinism is answered by the grammar rather than by analysis	True, unconditionally. No clock, no I/O, no randomness, no floats, no unbounded loops, no user recursion - all syntactic.	linear in document size; genuinely milliseconds
Termination is a syntactic check	True, with an asterisk. No recursion plus only a bounded map means every evaluation halts - but the bound is the input: iterating document lines is linear in the number of lines. “Bounded time and memory” means bounded in the declared input, which is only a promise if inputs are capped.	linear; needs a declared payload cap per profile
Exhaustive matching	True and cheap - and free once value domains are declared (RFC 0004).	linear
Type physics (no adding hours to kronor, no cross-kind identifiers)	True and cheap - ordinary static typing with units.	linear
Ownership and linearity (use-after-move is a compile error)	True and cheap - the technique is industrially proven.	near-linear
Conservation (nothing minted or vanished)	True and cheap by the right method: place invariants, not state-space search (RFC 0008).	linear algebra over the effect matrix
Pool safety - no event sequence drives a pool negative or past capacity	True but not cheap in the worst case. This is a coverability question on a vector addition system: EXPSPACE-complete. Full reachability is decidable and Ackermann-complete.	worst case astronomical; practical case below
Dead joins and unreachable branches as lint findings	Same family, same costs.	as above
“The state space is finite after all”	False in general. Three exits: unlimited-capacity pools, append-only registers that guards read, and unbounded event timestamps feeding rate buckets. True on the bounded fragment only.	n/a

Why the expensive one is fine in practice

Real contracts are not adversarial Petri nets. Three properties collapse the cost, and they deserve to be named rather than silently relied on:

1. Monotonicity. In almost every contract, draws only decrease availability within a period; no cycle refills a pool from nothing. A monotone system’s safety question yields to an invariant instead of a search.
2. Smallness. Pools per contract are single digits. The worked corpus is nowhere near an interesting complexity threshold.
3. Declared capacities. Every bound is written on the face of the document, so the invariant to prove is given rather than inferred. That is the difference between verifying a program and checking a declaration.

The honest formulation: the linter proves safety by invariant, and falls back to bounded model checking with a declared bound. It never claims to have explored an infinite space.

The proposal: a proof manifest

The standard’s own axiom is everything declared, nothing silent. Apply it to the linter’s own output. Genesis emits a signed proof manifest listing, per property, what was discharged for this contract and how:

proof-manifest:                       # emitted at genesis, sealed with the contract
  determinism        PROVEN    grammar
  totality           PROVEN    syntactic; document cap 5_000 lines (profile default)
  exhaustiveness     PROVEN    all matches covered
  type-physics       PROVEN
  linearity          PROVEN    ownership check clean
  conservation       PROVEN    place invariants; 3 pools, 4 boundary accounts
  pool-safety        PROVEN    invariant method (monotone draws)
  ceiling-safety     BOUNDED   model-checked to depth 10_000 events
  dead-joins         PROVEN    2 joins, both reachable
  fragment-exits     DECLARED  pool support.tickets is unbounded (non-money)

Three consequences worth the ink:

• A signer sees which promises they are actually getting, for this contract, instead of trusting a sentence about the language.
• BOUNDED and DECLARED are honest words that appear on the artifact. A contract leaving the checkable fragment cannot do so quietly.
• The manifest is diffable across versions. An amendment that downgrades PROVEN to BOUNDED is a visible regression - exactly the kind of change a counterparty should have to notice before signing.

The precedent is industrial: published assurance levels in high-integrity software exist precisely because “verified” alone means nothing; a language’s explicitly marked escapes from its checked fragment are the same idea in miniature; and bounded analysis tools have long labelled their bounds rather than implying completeness.

Two edits to the standard this implies

1. The finiteness footnote gets a scope. The satisfying claim - that this is a finite machine whose states are counted in pool balances - holds when every pool is bounded and no guard reads an unbounded register. Say that, then say what happens otherwise: the linter reports declared exits and the manifest renders them.
2. The nothing-crashes law gets its asterisk. “Bounded time and memory” becomes “bounded in the size of the declared input”, plus a profile obligation to declare input caps - otherwise a one-million-line invoice is a denial of service against a machine whose first property is that it cannot hang.

Honest creaks

1. A proof manifest is a new artifact class - one more thing to sign, version and render. It earns its place only if the linter genuinely emits it rather than a human writing it by hand.
2. “Proven by invariant” needs the invariants published, or it is an appeal to authority. The manifest should carry the invariant expressions, so a third party’s linter can check them - which is the whole point of an open standard.
3. Bounded checking picks a bound, and every bound is arbitrary. Declaring it is the mitigation; hiding it is the failure.
4. This makes the standard look weaker on paper. It is not weaker - the properties are unchanged. But a competitor quoting our own qualified table back at us is a real, if mild, cost of honesty. Worth paying.

This RFC is exploratory. It is published as a basis for discussion, not as normative text; where it touches the standard, the standard governs until a decision is recorded.