docs: add home, install, reference, philosophy, tooling and about pages

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>

Author: nos1dot618

content/about.md

@@ -0,0 +1,48 @@
+---
+title: About
+description: Where Lambda Discipline comes from, how it is built, and how to take part.
+---
+
+# About
+
+Lambda Discipline is an open-source functional programming language: lazy,
+statically typed and built directly on the lambda calculus. It is developed in
+the open by the [lambda-discipline](https://github.com/lambda-discipline)
+organization on GitHub.
+
+## History
+
+The language has been implemented more than once, and each version has
+learned from the last:
+
+* A first [Rust implementation](https://github.com/lambda-discipline/lambda-discipline-rust-legacy),
+  now archived.
+* A [C++ interpreter](https://github.com/lambda-discipline/lambda-discipline-cpp)
+  with a REPL, also archived.
+* The [current implementation](https://github.com/lambda-discipline/lambda-discipline),
+  a rewrite in Rust with full Hindley-Milner inference, call-by-need
+  evaluation, immutable lists, a redesigned set of builtins and a compiler
+  pipeline built to grow new backends.
+
+## Taking part
+
+Bug reports, language proposals and pull requests are welcome. Start with the
+[contributing guide](https://github.com/lambda-discipline/lambda-discipline/blob/master/CONTRIBUTING.md),
+and please follow the
+[code of conduct](https://github.com/lambda-discipline/lambda-discipline/blob/master/CODE_OF_CONDUCT.md).
+Security issues should be reported as described in the
+[security policy](https://github.com/lambda-discipline/lambda-discipline/blob/master/SECURITY.md).
+
+## This website
+
+The site is built by a small Python script from the
+[lambda-discipline.github.io](https://github.com/lambda-discipline/lambda-discipline.github.io)
+repository. Every day it checks the language repository for new commits, and
+when there are any it rebuilds: the [builtin reference](/builtins/) comes from
+`lbd docs --json`, and every [example](/examples/) is run by the current
+interpreter so the output you see is the output you'll get.
+
+## License
+
+Lambda Discipline and this website are released under the
+[MIT license](https://github.com/lambda-discipline/lambda-discipline/blob/master/LICENSE.txt).

content/index.md

@@ -0,0 +1,56 @@
+---
+title: Lambda Discipline
+template: home.html
+---
+
+```lbd
+-- Types are inferred; annotations are checked.
+fibonacci : Number -> Number = \n.
+    (if (lt n 2) n (add (fibonacci (sub n 1)) (fibonacci (sub n 2))))
+
+compose = \f. \g. \x. (f (g x))          -- (a -> b) -> (c -> a) -> c -> b
+
+(println (map fibonacci (range 0 10)))   -- [0, 1, 1, 2, 3, 5, 8, 13, 21, 34]
+(println ((compose show (mul 2)) 21))   -- 42
+```
+
+<ul class="features">
+  <li><strong>Lambdas, and little else</strong>Programs are applications of <code>\x. body</code> functions, written as S-expressions. The whole grammar fits on a postcard.</li>
+  <li><strong>Inferred types</strong>Hindley-Milner inference with let-polymorphism. Write annotations when they help you; the checker holds them to their word.</li>
+  <li><strong>Lazy by default</strong>Call-by-need evaluation: arguments are evaluated only when used, and at most once. Tail calls run in constant space.</li>
+  <li><strong>Immutable data</strong>Lists are persistent vectors. Every operation returns a new list and leaves the old one exactly as it was.</li>
+  <li><strong>Errors that help</strong>Several diagnostics per run, each pointing at the code that caused it, with "did you mean" suggestions.</li>
+  <li><strong>A real compiler</strong>Parser, resolver, type checker and a Core IR in front of a lazy abstract machine, with room for more backends.</li>
+</ul>
+
+## A first program
+
+Save this as `hello.lbd`:
+
+```lbd
+greet : String -> String = \name. (concat "Hello, " name)
+
+(println (greet "World"))
+```
+
+and run it:
+
+```text
+$ lbd run hello.lbd
+Hello, World
+```
+
+Or start `lbd` with no arguments for a REPL, where `:type` shows the type of
+any expression:
+
+```text
+λ> :type (map (add 1))
+(map (add 1)) : List<Number> -> List<Number>
+```
+
+## Where to next
+
+* [Install](/install/) the interpreter.
+* Read the [language reference](/reference/) and the [builtins](/builtins/).
+* Browse the [examples](/examples/), from Hello World to Advent of Code.
+* Find out [why the language looks the way it does](/philosophy/).

content/install.md

@@ -0,0 +1,59 @@
+---
+title: Install
+description: Install the lbd interpreter with Cargo, or build it from source.
+---
+
+# Install
+
+Lambda Discipline is a single binary, `lbd`, that runs programs, type-checks
+them and hosts the REPL.
+
+## With Cargo
+
+You need [Rust](https://www.rust-lang.org/tools/install) 1.85 or newer.
+
+```bash
+cargo install --git https://github.com/lambda-discipline/lambda-discipline
+```
+
+This puts `lbd` in `~/.cargo/bin`, which `rustup` already added to your `PATH`.
+
+## Prebuilt binaries
+
+Tagged versions are published on the
+[releases page](https://github.com/lambda-discipline/lambda-discipline/releases)
+for Linux (x86-64), macOS (Apple silicon) and Windows (x86-64). Download the
+archive for your platform, extract it, and put `lbd` somewhere on your `PATH`.
+
+## From source
+
+```bash
+git clone https://github.com/lambda-discipline/lambda-discipline
+cd lambda-discipline
+cargo build --release
+```
+
+The binary is `target/release/lbd`. Run the test suite with `cargo test`.
+
+## Check that it works
+
+```bash
+lbd --version
+```
+
+```bash
+lbd run examples/hello_world.lbd
+```
+
+## Using it
+
+| Command | What it does |
+| --- | --- |
+| `lbd run <file>` | Type-check and run a program. The exit code is 1 on any error. |
+| `lbd check <file>` | Type-check without running. |
+| `lbd check <file> --emit <stage>` | Print an intermediate representation: `tokens`, `ast`, `types` or `core`. |
+| `lbd repl`, or just `lbd` | Start an interactive session. |
+| `lbd docs [name] [--json]` | Show the [builtin reference](/builtins/). |
+
+Next, set up your [editor](/tooling/) or start with the
+[language reference](/reference/).

content/philosophy.md

@@ -0,0 +1,82 @@
+---
+title: Philosophy
+description: The ideas behind Lambda Discipline, and why the language looks the way it does.
+---
+
+# Philosophy
+
+> A language should be small enough to hold in your head, and strict enough
+> that what you hold there is true.
+
+Lambda Discipline begins with the lambda calculus, the smallest language that
+can express any computation: variables, functions of one argument, and
+application. Everything else is there to make that core pleasant to write and
+safe to run. Where convenience and coherence disagree, coherence wins.
+
+## The lambda is the unit of thought
+
+There are no statements, no loops and no special forms. A program is
+definitions and applications of `\x. body` functions, and each application is
+an S-expression whose shape *is* its meaning: `(f x y)` applies `f` to `x`,
+then to `y`. A grammar this small has no corners to memorize. You learn it once
+and then think only about your problem.
+
+Functions take one argument at a time, so partial application is free. The
+builtins are designed for it: the data a function works on always comes last,
+which makes `(map (add 1))`, `(filter (lt 0))` and `(split ",")` complete,
+meaningful functions on their own.
+
+## Discipline means types
+
+The *discipline* is the type system. Every program is checked with
+Hindley-Milner inference before a single expression runs, and a program that
+doesn't type-check doesn't run. There are no warnings to ignore.
+
+Inference keeps the discipline from becoming bureaucracy. You write
+annotations where they say something useful to a reader, and the checker works
+out the rest, always finding the most general type. When you do write an
+annotation, it is a contract: its type variables are rigid, so a function
+can't quietly claim to be more general than it is.
+
+## Laziness is the honest default
+
+Arguments are evaluated when they are needed, and only once. With laziness,
+`if`, `and` and `or` need no special treatment: they are ordinary functions
+that simply don't touch the branch they don't take. Control flow is just
+another thing you can define, pass around and partially apply.
+
+Laziness asks for a runtime that respects it, so tail calls run in constant
+space, deep recursion is bounded by memory rather than a fixed stack, and a
+value that depends on itself is reported instead of hanging.
+
+## Values don't change
+
+Lists are immutable persistent vectors. Adding, removing or reading an element
+returns a new list in logarithmic time and leaves the original exactly as it
+was. A name means one thing for its whole life, which is what makes laziness,
+sharing and equational reasoning safe.
+
+## Errors are part of the interface
+
+A language is used mostly while it is telling you that you're wrong. Lambda
+Discipline reports every independent error it finds in one run, points at the
+exact code responsible, and suggests the name you probably meant. Runtime
+errors point at the call that failed. Nothing crashes with a stack trace from
+the implementation.
+
+## Built like a compiler
+
+Under the interpreter is a conventional compiler pipeline, the shape of rustc
+or GHC: a lexer and parser, name resolution, type inference, and a Core IR that
+is closure-converted and uncurried. Today that IR feeds a lazy abstract
+machine. Tomorrow it can feed a transpiler, a virtual machine or native code
+without the front end changing. Builtins are declared once, with their type and
+documentation, and every stage reads that one declaration. The
+[builtin reference](/builtins/) on this site is generated from it.
+
+## Free to improve
+
+Lambda Discipline is young, and it isn't bound by compatibility with its own
+past. Its current implementation is a ground-up rewrite that renamed builtins,
+tightened the type system and changed the syntax wherever doing so made the
+language more coherent. It will keep doing that while it's young.