std/invariants: Rules Only Inference Can Check

Koru’s compiler decides a fixed set of questions. Did the obligation discharge. Does the shape match. Is this proc pure. Each has a subject — a value, a binding, a call — and the checker walks to it and renders a verdict.

Now try to state this one:

Comments are written in English, not Norwegian.

There is nothing to walk to. It is not about a value or a call; it is about every comment that exists and every comment that will be written. Or this one:

This diff adds a fallback where the charter wants an assertion.

That is about a change, not a program. No compiler will ever see it.

These rules are real, they are load-bearing, and until now they lived in CLAUDE.md files, in review habits, and in people’s heads — which is to say they were forgotten at exactly the rate you would expect.

Declare, don’t enforce

std/invariants gives them a place to live: inside the source, next to the code they constrain.

import std/io
import std/invariants

std/invariants:inferred {
  "name": "comment-language",
  "tags": ["git-gate"],
  "rule": "Comments are written in English, not Norwegian."
}

std/invariants:aspirational {
  "name": "no-silent-truncation",
  "tags": ["git-gate"],
  "rule": "No emitter drops elements without a diagnostic."
}

std/io:print.ln("flow ran once")

The program prints flow ran once. The invariants cost it nothing — they are [comptime|norun], which means data in the AST, never a step in the flow.

The rule is written in prose on purpose. A consumer that reads natural language finds things a formal target vocabulary would have excluded before it ever looked. Weak links are the feature.

Two dispositions, opposite gradients

There are two tors, not one with a kind: field, and the reason is that the name carries the only bit that matters:

inferred — permanent by nature. Nothing will ever make “comments are in English” a compiler check. There is no pressure, and growth is good: a large inferred set is a well-described project.

aspirational — debt by construction. The author means this to become a real check and hasn’t built it yet. Growth is a smell, and a gate is entitled to say so.

They differ by one undecidable bit: does the author intend this to become code. Nobody can recover that later by re-reading the rule — you would be guessing at intent. So it is stated at the moment of writing, by choosing the word, or it is lost. Ship only inferred and every aspirational rule silently files as permanent, unrecoverably.

The module ships its reader

This is the whole difference between an invariant and a comment. A comment is prose a human might find. An invariant is enumerable:

$ koruc app.k invariants

inferred
  comment-language  ["git-gate"]
    app.k:5
    Comments are written in English, not Norwegian.

aspirational
  no-silent-truncation  ["git-gate", "review"]
    app.k:11
    No emitter drops elements without a diagnostic.

1 inferred, 1 aspirational

The command is itself declared in the module, through the same command.declare mechanism koruc --help uses to discover flags. Nothing is hardcoded: a consumer finds invariants by parsing the program. It walks every module the program imports, so a library’s own rules are visible rather than silently dropped.

Enumerable is the floor, and it is deliberately the only thing built. A git gate is now a shell script somebody writes on a Tuesday, and this module never changes to get one. Censuses, drift detection, per-tag gating — all downstream, all optional, none of them load-bearing for the surface to be useful today.

Where this sits

The companion post, Distributed Invariants as Obligations, walks how far the type system reaches: a stale owner that cannot write, an acknowledgement that cannot outrun its durability proof. It ends at a boundary — an obligation is a claim about one value’s lifetime, and some rules are relations the checker cannot state.

std/invariants is what lives past that boundary. Not a weaker checker: a different kind of claim, one whose reader was never going to be an algorithm.

Increasingly that reader is an agent, which is the part that makes this worth shipping now rather than eventually. An agent reading a diff can evaluate “comments are written in English” perfectly well. What it cannot do is guess which rules this project holds. Now it can ask.