Skip to content

docs: the spec's front door points at the right file, and no page for readers carries notation - #228

Merged
lex00 merged 3 commits into
mainfrom
docs/reading-order
Sep 19, 2026
Merged

lex00 merged 3 commits into
mainfrom
docs/reading-order

Conversation

@lex00

@lex00 lex00 commented Sep 19, 2026

Copy link
Copy Markdown
Contributor

Came out of asking whether spec notation leaks onto the site. It doesn't — the pages for readers who are not implementers carry no ⊢, no ⇓, no T(B), nothing. That boundary was already intact.

The problem is the opposite one.

The site's reading order describes a spec that stopped existing at #168

Read judgments.md next; it owns the F-* judgments: J1 expression evaluation and J2 the per-file verdict; J3 the identity-taint fixpoint and J4 properties and observables. Its preamble states the objective the whole mechanism serves.

judgments.md has been a 14-line index since the split. It owns none of that. The page also promised "each of those five ends with a non-normative Rationale section" — extracted to rationale.md by the same change — and omitted rules.md from the order entirely.

And it never mentioned objective.md, which is the part that matters

spec/README.md is current and says:

objective.md states it with the two profiles an implementation may claim and the notation the judgments are written in. Start there.

The site's version of that instruction didn't exist. So a reader meeting Γ, H ⊢ e ⇓ v for the first time had no signpost to the guide that reads it — the guide added by #202, which claims to be self-contained, sitting in a file the reading order never named.

That is a complete explanation for "I can't read the formulas": the front door pointed at an empty room and never mentioned the one with the instructions in it.

Fixed

Order now matches spec/README.md: objective first, named explicitly as where the notation guide lives and what it covers, then the nine rule files in order, then rationale, inventory, prior art, changelog.

Why the gate missed it

#181's citation check fires when a sentence cites a spec file and names a rule identifier. These sentences named F-* as a glob, not a rule, so nothing matched. Worth knowing the check has that shape — it catches a wrong file for a named rule, not a wrong file for a family.

Also

ι leaves conformance/corpus.md — the corpus runs "under isolation" rather than "under ι = isolated". I added that symbol yesterday and it buys nothing outside the specification. That was the only notation anywhere outside the normative text.

List item openings vary instead of all ten starting with a link, which the prose gate reads as anaphora and which is worse writing regardless.

Verification

121 tests in 19 files, prose lint 51 with no regressions, npm run docs:build clean, and a re-scan confirms no notation symbols outside /spec/.

🤖 Generated with Claude Code

https://claude.ai/code/session_01AzfJnYw9p6rAxhJqXK3CPv

lex00 and others added 2 commits September 19, 2026 15:17
…tation guide exists

"Reading the specification" described a document set that stopped existing at
#168. It sent a reader to `judgments.md` for "the `F-*` judgments: J1, J2, J3
and J4" and for "the objective the whole mechanism serves". That file has been
a 14-line index since the split, and it owns none of those. It also promised
"each of those five ends with a non-normative Rationale section", which #168
extracted into `rationale.md`. `rules.md` was missing from the order entirely.

`objective.md` was not mentioned at all, and that is the part that matters.
`spec/README.md` says "Start there" and says why: the objective, the two
profiles, and the notation the judgments are written in. A reader arriving at
`Γ, H ⊢ e ⇓ v` had no signpost to the guide that reads it, because the page
whose job is the reading order never said the guide was there.

The order now matches `spec/README.md`: objective first and named as the
notation guide, then the nine rule files, then rationale, inventory, prior art
and the changelog.

The citation gate did not catch this. It fires when a sentence cites a spec
file and names a rule identifier, and these sentences named `F-*` as a glob
rather than a rule.

Also here: `ι` leaves the conformance page. The corpus runs "under isolation"
rather than under `ι = isolated`. The symbol is the specification's and buys
nothing outside it. Nothing else on the site carries notation — the pages for
readers who are not implementers have none of it, which is the boundary this
keeps.

List openings vary rather than every item starting with a link, which the
prose gate reads as anaphora and which is worse writing either way.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01AzfJnYw9p6rAxhJqXK3CPv
`fold(generate(v)) = v` and `fold(generate(v)) = revive(v)` were on a page
written for readers who are not implementers, twice: once in the opening and
once in the limit I added yesterday. The sentence before the first one already
said it in English — an existing artifact becomes TypeScript that folds back
to exactly the data it came from — so the equation restated it in a notation
the rest of the page does not use.

Both are prose now. Under `data-host` you get back exactly what you put in,
and under `full` you get it as live objects instead. `F-Val-Source` states
both forms and the page already links it.

The scan that reported these pages clean was wrong. It matched Unicode
notation and nothing else, so plain-ASCII equations passed it. Checking for
backticked spans containing `=` or `(` finds them and finds nothing else on
any other page: what it turns up elsewhere is shell commands and identifiers.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01AzfJnYw9p6rAxhJqXK3CPv
@lex00 lex00 changed the title docs: the spec's front door points at the right file, and says the notation guide exists docs: the spec's front door points at the right file, and no page for readers carries notation Sep 19, 2026
The boundary held by habit. Everything outside `docs/content/spec/` is read by
someone who has not met any of this, and it slipped twice in one week, both
times from an author who had just been editing the specification: `ι =
isolated` on a conformance page, and `fold(generate(v)) = revive(v)` on the
round-trip page in both its opening and its limit.

`spec/site-readability.test.ts` checks three shapes on every authored page
outside the specification's own section.

  Judgment and set notation. Nothing a reader of these pages has met.

  Equations. The scan that reported those pages clean looked only for notation
  characters, so a plain-ASCII equation passed it. The shape that catches one
  and not a shell command is a lowercase single-letter argument.

  Rule identifiers, counted per page, shrink-only. Naming a rule once so a
  reader can find it is fair. A page that reads like the specification is not,
  and that happens one identifier at a time.

What it found, beyond the equations already removed: `no-execution.md` carried
nine, four of them a bulleted list of `F-Val-Fate`, `F-Eval-CallEager`,
`F-Eval-CallMethod` and `F-Call` step 6 with the English already beside each.
The English stays and the identifiers go, along with `F-IsolatedRefusal`,
`F-Host-Interface` and two `F-Profile-DataHost`. Four left: the rule this page
is about, named where a reader would look for it.

Every check is mutation-tested. Putting a judgment, an equation and two
identifiers into the landing page fails all three.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01AzfJnYw9p6rAxhJqXK3CPv
@lex00
lex00 merged commit f76bd82 into main Sep 19, 2026
3 checks passed
@lex00
lex00 deleted the docs/reading-order branch September 19, 2026 21:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant