Docs: language-neutral behavior pages, generated per-language references, and executed examples

[lan17]

Summary

The documentation site should be built in three layers with different processes: behavior documentation written once and checked against the specification, per-language API reference generated by each language's native tool, and short per-language guides whose examples are compiled and run in CI. An agent may draft prose and examples; the machine decides whether what it wrote is true. This issue records that target, the gates that make it hold, and the process for adding a language. It complements #165, which covers the specification itself.

Where the documentation is today

The site is VitePress over 14 hand-written Markdown pages under docs/, about 3,700 lines, built by make docs (vitepress build docs) and deployed to GitHub Pages by .github/workflows/docs.yaml on pushes to main. The pages were drafted with an LLM and reviewed by hand.

Fact	Today
Pages describing behavior (concepts, keys, invalidation, stale-on-error, shadow validation, coalescing, observability, Redis, configuration)	Language-neutral in substance, TypeScript in vocabulary and examples
Pages that are TypeScript-specific	api.md (entry points, constructor, client factories), upgrading.md (TypeScript API renames), most of redis.md (DialCacheRedisClient, node-redis and valkey-glide clients, JsonSerializer) and observability.md (DialCacheMetricsAdapter, Prometheus and Datadog adapters), and parts of getting-started.md
Fenced code blocks	25 ts blocks across the site, plus 11 bash and 17 text blocks; no code in any language other than TypeScript
Go documentation	go/README.md, 224 lines, one Go code block; no page on the site. The package has one runnable Example in go/example_test.go that go test executes and go doc renders
Snippet verification	None for the site. No test compiles or runs a docs/ example; the block in go/README.md is likewise unchecked
API surface check	None. Nothing enumerates the Go exported surface. formal/check-go-parity.mjs snapshots TypeScript source declarations for the parity ledger and scripts/test-package.mjs asserts a fixed list of packed exports, but nothing compares either with what is documented
Behavior-to-page check	Partial. formal/source-audit.json fingerprints every page under docs/ (file hash plus a per-heading inventory) and tags each heading with the contract IDs it covers; formal/check-source-audit.mjs fails make audit on an unreviewed edit or an unknown ID. It does not require that every contract is documented (C04, C10, C15, C19 and C46 are cited by no page) or that one page owns a contract (49 IDs appear on several pages)

The consequence is that the docs are good prose whose only mechanical tie to the code is the freshness audit: a page edit fails make audit until a human refreshes its contract tags, but nothing checks that the prose or the examples are true. Adding a second language by the same method doubles the surface that can drift.

Target: three layers, three processes

1. Behavior documentation is written once and is language-neutral. Concepts, keys, invalidation, stale-on-error, shadow validation, coalescing, configuration semantics and observability semantics describe DialCache, not a port. The prose refers to concepts and contract names rather than TypeScript identifiers. Code examples are tabbed blocks with one tab per language. With the kernel model from #165 there is one specification document to derive these pages from.

2. API reference is generated per language by the native tool and never hand-written. TypeDoc or API Extractor for TypeScript, go doc and pkg.go.dev for Go, and the equivalent for any later language. Doc comments on exported symbols are the source. The generated reference is part of make docs and is what the site links to as "API reference" for each language.

3. Per-language guides are short and their examples are real files. Getting started, installing a client integration, language idioms. Every snippet lives in an examples directory for that language, is compiled and run in CI against the conformance fixtures, and is pulled into the Markdown by marker. The Markdown never contains an example that the build did not execute.

One page generated from the specification

formal/semantic-cases.json already holds 262 named behavior cases, each with rule text and a citation of its Quint invariant or regression and of the implementation evidence. A generated behavior catalogue page, one row per case linking to the regression and to each port's evidence, is language-neutral, costs nothing per port, and is the most trustworthy page the site can have. It is the documentation counterpart of the conformance corpus: the same source feeds every port.

Gates

• API surface parity. For each language, the set of exported public symbols equals the set of documented symbols. A new export without a doc comment fails the build; a documented symbol that does not exist fails the build.
• Snippet execution. Every example in the site compiles and runs for its language in CI. Behavior examples run against the same fixtures the conformance drivers use, so an example that shows wrong behavior fails.
• Contract-to-page mapping. Every obligation in formal/CONTRACTS.md (C01 to C60, W01 to W09) is owned by one behavior page and may be referenced from others. formal/source-audit.json already tags each docs/ heading with contract IDs and fingerprints the page; the gate adds the missing direction: an obligation cited by no page fails, and each obligation names its owning page.
• Anchor and external link check. VitePress already fails the build on a dead internal page link; the check extends to #anchor targets, external URLs and links into the generated references.

Process for a new language

1. Add the native reference generator to make docs. Automatic.
2. Add a tab for the language to each behavior page. An agent drafts the snippets from the specification and the behavior pages, never from another language's prose; CI compiles and runs them.
3. Draft the getting-started guide from a written docs-porting checklist kept with formal/PORTING.md. A human reviews the prose.
4. Run the gates. Nothing ships until API parity, snippet execution, the contract mapping and the link check pass.

Acceptance criteria

• Behavior pages (concepts, keys, invalidation, stale-on-error, shadow validation, coalescing, configuration, observability semantics) contain no language-specific identifiers in prose and carry one example tab per supported language.
• make docs generates the API reference for every supported language from doc comments and fails on an undocumented export.
• Every fenced example on the site is sourced from a file that CI compiles and runs.
• A generated behavior catalogue page exists and is rebuilt from semantic-cases.json on every docs build.
• The contract-to-page mapping and the anchor and external link check run in the documentation workflow.
• The Go port has a getting-started guide and an API reference on the site, produced by this process, as the proof that the process works for a second language.

Reference points

• Formal: converge the Quint specification on one kernel model with profile instances #165 records the target for the specification these pages derive from.
• docs/.vitepress/config.mts holds the current navigation; .github/workflows/docs.yaml builds and deploys the site.