Site

site/.gitignore

@@ -1,7 +1,6 @@
 node_modules
 dist
 .astro
-src/content/docs/index.md
 src/content/docs/getting-started.md
 src/content/docs/spec.md
 src/content/docs/spec-dafny.md
@@ -10,4 +9,6 @@ src/content/docs/tools.md
 src/content/docs/design.md
 src/content/docs/architecture-narrowing.md
 src/content/docs/agents.md
+src/content/docs/subset.md
+src/content/docs/case-studies.md
 src/content/docs/howto_greenfield.md

site/astro.config.mjs

@@ -48,17 +48,17 @@ function rehypeRepoLinks() {
 // only touch links whose visible text IS a bare *.md filename, so intentional
 // text like `[SPEC.md §2]` or `[TOOLS.md#narrow-rules]` is left untouched.
 const LINK_NAMES = {
-  "/": "Overview",
-  "/subset/": "Overview (Subset)",
-  "/getting-started/": "Getting Started",
-  "/howto_greenfield/": "Greenfield tutorial",
+  "/case-studies/": "Case studies & examples",
+  "/subset/": "Supported TypeScript subset",
+  "/getting-started/": "Getting started in an existing codebase",
+  "/howto_greenfield/": "Start a new project",
   "/spec/": "Specification",
   "/spec-dafny/": "Dafny backend spec",
   "/spec-lean/": "Lean backend spec",
-  "/tools/": "Tools",
+  "/tools/": "Toolchain architecture",
   "/design/": "Design",
   "/architecture-narrowing/": "Narrowing architecture",
-  "/agents/": "Agents",
+  "/agents/": "Guidance for agents",
 }
 const BARE_FILENAME = /^[A-Za-z0-9_]+\.md$/
 
@@ -91,11 +91,12 @@ export default defineConfig({
       social: [{ icon: "github", label: "GitHub", href: "https://github.com/midspiral/LemmaScript" }],
       sidebar: [
         {
-          label: "Getting started",
+          label: "Start here",
           items: [
-            { label: "Overview (Subset)", link: "/subset/" },
-            { label: "Overview (Brownfield)", link: "/getting-started/" },
-            { label: "Howto (Greenfield)", link: "/howto_greenfield/" },
+            { label: "What is LemmaScript?", link: "/" },
+            { label: "Installation", link: "/installation/" },
+            { label: "How the loop works", link: "/how-the-loop-works/" },
+            { label: "How to: Brownfield", link: "/getting-started/" },
           ],
         },
         {
@@ -117,22 +118,25 @@ export default defineConfig({
           ],
         },
         {
-          label: "Specification",
+          label: "Reference",
           items: [
-            { label: "Overview", link: "/spec/" },
+            { label: "CLI (lsc)", link: "/reference/cli/" },
+            { label: "Supported TypeScript subset", link: "/subset/" },
+            { label: "Specification", link: "/spec/" },
             { label: "Dafny backend", link: "/spec-dafny/" },
             { label: "Lean backend", link: "/spec-lean/" },
           ],
         },
-        { label: "Tools", link: "/tools/" },
         {
-          label: "Design",
+          label: "Under the hood",
           items: [
             { label: "Design rationale", link: "/design/" },
+            { label: "Toolchain architecture", link: "/tools/" },
             { label: "Architecture: narrowing", link: "/architecture-narrowing/" },
+            { label: "Guidance for agents", link: "/agents/" },
+            { label: "Case studies & examples", link: "/case-studies/" },
           ],
         },
-        { label: "Agents", link: "/agents/" },
       ],
     }),
   ],

site/scripts/sync-docs.mjs

@@ -12,24 +12,28 @@ const here = dirname(fileURLToPath(import.meta.url))
 const ROOT = join(here, "..", "..") // repo root: site/scripts -> site -> repo
 const OUT = join(here, "..", "src", "content", "docs")
 
-// Which root docs become site pages.
+// Which root docs become site pages. `title` (optional) overrides the H1-derived
+// page title so synced pages can carry reader-facing names without editing the
+// repo files themselves.
 const DOCS = [
-  { src: "README.md", out: "index.md" }, // home / overview
+  // The site homepage (index.md) is hand-written; the README syncs to its own
+  // page under "Under the hood" as the case-studies/overview reference.
+  { src: "README.md", out: "case-studies.md", title: "Case studies & examples" },
   { src: "SUBSET.md", out: "subset.md" },
-  { src: "GETTING_STARTED.md", out: "getting-started.md" },
+  { src: "GETTING_STARTED.md", out: "getting-started.md", title: "Getting started in an existing codebase" },
   { src: "TUTORIAL_GREENFIELD.md", out: "howto_greenfield.md" },
   { src: "SPEC.md", out: "spec.md" },
   { src: "SPEC_DAFNY.md", out: "spec-dafny.md" },
   { src: "SPEC_LEAN.md", out: "spec-lean.md" },
-  { src: "TOOLS.md", out: "tools.md" },
+  { src: "TOOLS.md", out: "tools.md", title: "Toolchain architecture" },
   { src: "DESIGN.md", out: "design.md" },
   { src: "ARCHITECTURE_NARROWING.md", out: "architecture-narrowing.md" },
-  { src: "AGENTS.md", out: "agents.md" },
+  { src: "AGENTS.md", out: "agents.md", title: "Guidance for agents" },
 ]
 
 // filename -> site route, for rewriting cross-doc links so site nav works.
 const ROUTES = {
-  "README.md": "/",
+  "README.md": "/case-studies/",
   "SUBSET.md": "/subset/",
   "GETTING_STARTED.md": "/getting-started/",
   "TUTORIAL_GREENFIELD.md": "/howto_greenfield/",
@@ -94,14 +98,14 @@ for (const d of DOCS) rmSync(join(OUT, d.out), { force: true })
 mkdirSync(OUT, { recursive: true })
 
 const broken = []
-for (const { src, out } of DOCS) {
+for (const { src, out, title: override } of DOCS) {
   const raw = readFileSync(join(ROOT, src), "utf8")
   const { title, body } = titleAndBody(raw)
   const rewritten = rewriteLinks(body)
   broken.push(...missingRepoLinks(src, rewritten))
   const target = join(OUT, out)
   mkdirSync(dirname(target), { recursive: true })
-  writeFileSync(target, `---\ntitle: "${esc(title)}"\n---\n\n${rewritten}`)
+  writeFileSync(target, `---\ntitle: "${esc(override ?? title)}"\n---\n\n${rewritten}`)
 }
 
 if (broken.length) {

site/src/content/docs/how-the-loop-works.md

@@ -0,0 +1,66 @@
+---
+title: "How the loop works"
+description: "Contracts, checks, and iteration — the concepts behind LemmaScript in five minutes, no setup required."
+---
+
+<!-- Hand-written manual page (concepts; no setup needed). -->
+
+Four ideas explain almost everything else in these docs.
+
+## 1. A contract is the function's API for correctness
+
+Above a function, `//@ ` annotations state what it needs and what it promises:
+
+```typescript
+//@ contract Never lets the charge exceed the available balance.
+//@ requires balance >= 0
+//@ requires amount >= 0
+//@ ensures amount <= balance ==> \result === balance - amount
+//@ ensures amount > balance ==> \result === 0
+function charge(balance: number, amount: number): number { /* … */ }
+```
+
+- `requires` — what callers must guarantee coming in
+- `ensures` — what the function guarantees going out (`\result` is the return value)
+- `contract` — the same promise in plain English, for the human reviewer
+
+These are the three you'll see most. The full annotation list is in
+[the specification](/spec/#2-the---annotation-language).
+
+The implementation stays ordinary TypeScript. Contracts are comments, so they cost
+nothing at runtime and change nothing about how the code builds or ships.
+
+## 2. `lsc check` decides, it doesn't sample
+
+Testing runs the code on chosen inputs; `lsc check` translates the function and its
+contract to a prover (Dafny by default) and asks whether the implementation meets
+the spec **for every input the contract admits**. The answer is a verdict, not a
+survey: correct, or not correct yet — with the failing obligation to point at.
+
+The two do different jobs, and both matter: contracts settle the core logic;
+tests remain the right tool for integration, I/O, and everything outside the
+verified boundary.
+
+## 3. "Not correct yet" is a loop state, not a bug report
+
+When a check fails, either the code doesn't do what the contract says, or the
+contract doesn't say what you meant. The loop is: adjust one of them, re-run,
+repeat. Agents drive this loop well — with the
+[skills](https://github.com/midspiral/lemmascript-skills) installed, an agent writes the contract and the code
+together and iterates until the check passes, so what surfaces is correct code.
+Your job shifts to reviewing the contract: a few declarative lines that say
+exactly what was guaranteed.
+
+## 4. Generated files carry the proof work
+
+For the Dafny backend, `lsc` writes two files next to your source: `foo.dfy.gen`
+(always regeneratable — never edit) and `foo.dfy` (yours — helper lemmas and proof
+additions accumulate here; the difference from `.dfy.gen` must be additions-only,
+and `lsc check` enforces that). After editing the TypeScript, `lsc regen`
+three-way-merges the new generated code into `foo.dfy` so proof work is never lost.
+Precise rules live in the [Dafny backend spec](/spec-dafny/).
+
+## Next
+
+- [What TypeScript is supported](/subset/) — the subset the prover understands
+- [CLI reference](/reference/cli/) — every command in the loop

site/src/content/docs/index.md

@@ -0,0 +1,48 @@
+---
+title: "What is LemmaScript?"
+description: "TypeScript with syntax for contracts — an agent writes the contract and the code together, and only correct code ships."
+---
+
+<!-- Hand-written homepage (not synced). The repo README syncs to /case-studies/. -->
+
+LemmaScript is **TypeScript with syntax for contracts** — the way TypeScript is
+JavaScript with syntax for types. You (or your agent) write ordinary TypeScript and
+add `//@ ` annotations stating what a function must do. The `lsc` toolchain
+translates the code to a prover — Dafny or Lean 4 — and checks that the
+implementation actually meets the spec. Contracts add **zero runtime cost** and work
+on **existing codebases**, one function at a time.
+
+It's built agent-first: the agent writes the contract and the implementation
+together and iterates until the check passes. You review the contract — a few
+declarative lines — instead of the implementation.
+
+## What it looks like
+
+An agent splitting 10 three ways once floored each share and called it done:
+`[3, 3, 3]` — that's 9, not 10; a cent vanished. With a contract, that
+implementation can't survive:
+
+```typescript
+//@ contract Splits total across weights so every unit is accounted for.
+//@ requires total >= 0
+//@ requires weights.length >= 1
+//@ requires forall(k, 0 <= k && k < weights.length ==> weights[k] >= 0)
+//@ requires sum(weights) >= 1
+//@ ensures sum(\result) === total     // must sum to the whole
+function allocate(total: number, weights: number[]): number[] {
+  // the floor-and-forget version fails this ensures;
+  // the fix hands the leftover back out — and passes
+}
+```
+
+`lsc check` rejects the buggy version, the agent reads the failure and fixes the
+code, and only the correct version surfaces.
+
+## Where to start
+
+- **[Installation](/installation/)** — Node, Dafny, the `lsc` toolchain, and the agent skills
+- **[How the loop works](/how-the-loop-works/)** — the concepts in five minutes
+- **[Add to an existing codebase](/getting-started/)** — start with one small function
+
+Prefer the full story? Read the [design rationale](/design/), or see what's been
+built with it in the [case studies](/case-studies/).

site/src/content/docs/installation.md

@@ -0,0 +1,76 @@
+---
+title: "Installation"
+description: "Install the lsc toolchain from npm and add the agent skills — or clone the source kit with everything bundled."
+---
+
+<!-- Hand-written manual page. Twin: lemmascript-landing/src/pages/install.astro —
+     keep the two in lockstep when the install story changes. -->
+
+Two ways in. Use the **package** if you're using LemmaScript; take the **kit** if
+you're changing it.
+
+## Option A — the package
+
+The standard setup: the `lsc` toolchain from npm, plus the skills that teach your
+agent to drive it.
+
+### 1. Check the prerequisites
+
+- **Node.js ≥ 18**
+- **[Dafny ≥ 4.x](https://dafny.org/latest/Installation)** — the prover that does the checking
+- **git**
+
+```sh
+node -v          # ≥ 18
+dafny --version  # ≥ 4.x
+```
+
+For the optional Lean backend you'll also need **Lean 4** (managed via `elan`/`lake`).
+
+### 2. Install the package
+
+One global install puts `lsc` — and companions like `lsc claimcheck` — on your PATH:
+
+```sh
+npm install -g lemmascript
+```
+
+### 3. Add the skills
+
+Mount the [lemmascript-skills](https://github.com/midspiral/lemmascript-skills) repo
+at your agent's skills directory — e.g. `.claude/skills` for Claude Code. Your agent
+picks them up and drives the whole loop itself: contracts, checks, iteration.
+
+```sh
+git clone https://github.com/midspiral/lemmascript-skills <your/skills/dir>
+```
+
+### 4. Check something
+
+```sh
+lsc check --backend=dafny path/to/file.ts
+```
+
+## Option B — from source: lemmascript-kit
+
+Working on the toolchain itself, or want the tools and skills pinned together?
+[lemmascript-kit](https://github.com/midspiral/lemmascript-kit) bundles the toolchain
+source and the skills as git submodules — one clone, one setup script, skills
+already in place at `.claude/skills/`.
+
+```sh
+git clone --recurse-submodules https://github.com/midspiral/lemmascript-kit.git
+cd lemmascript-kit
+./setup.sh
+```
+
+Run the same commands straight out of the source tree (the skills write the CLI as
+`npx lsc`; in the kit, substitute this form or `npm link` the package):
+
+```sh
+npx tsx LemmaScript/tools/src/lsc.ts check --backend=dafny path/to/file.ts
+```
+
+## Next
+
+- [CLI reference](/reference/cli/) — every `lsc` command