docs: the spec's front door points at the right file, and no page for readers carries notation - #228
Merged
Merged
Conversation
…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
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
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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⇓, noT(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
judgments.mdhas 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 torationale.mdby the same change — and omittedrules.mdfrom the order entirely.And it never mentioned
objective.md, which is the part that mattersspec/README.mdis current and says:The site's version of that instruction didn't exist. So a reader meeting
Γ, H ⊢ e ⇓ vfor 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
ιleavesconformance/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:buildclean, and a re-scan confirms no notation symbols outside/spec/.🤖 Generated with Claude Code
https://claude.ai/code/session_01AzfJnYw9p6rAxhJqXK3CPv