diff --git a/README.md b/README.md
index 1ca8010..8a962ab 100644
--- a/README.md
+++ b/README.md
@@ -2,15 +2,22 @@
 
 A functional programming language with first-class effects, schema evolution, and behavioral types.
 
-## Vision
+## Philosophy
 
-Most programming languages treat three critical concerns as afterthoughts:
+**Make the important things visible.**
 
-1. **Effects** — What can this code do? (Hidden, untraceable, untestable)
-2. **Data Evolution** — Types change, data persists. (Manual migrations, runtime failures)
-3. **Behavioral Properties** — Is this idempotent? Does it terminate? (Comments and hope)
+Most languages hide what matters most: what code can do (effects), how data changes over time (schema evolution), and what guarantees functions provide (behavioral properties). Lux makes all three first-class, compiler-checked language features.
 
-Lux makes these first-class language features. The compiler knows what your code does, how your data evolves, and what properties your functions guarantee.
+| Principle | What it means |
+|-----------|--------------|
+| **Explicit over implicit** | Effects in types — see what code does |
+| **Composition over configuration** | No DI frameworks — effects compose naturally |
+| **Safety without ceremony** | Type inference + explicit signatures where they matter |
+| **Practical over academic** | Familiar syntax, ML semantics, no monads |
+| **One right way** | Opinionated formatter, integrated tooling, built-in test framework |
+| **Tools are the language** | `lux fmt/lint/check/test/compile` — one binary, not seven tools |
+
+See [docs/PHILOSOPHY.md](./docs/PHILOSOPHY.md) for the full philosophy with language comparisons and design rationale.
 
 ## Core Principles
 
diff --git a/docs/PHILOSOPHY.md b/docs/PHILOSOPHY.md
new file mode 100644
index 0000000..611bd20
--- /dev/null
+++ b/docs/PHILOSOPHY.md
@@ -0,0 +1,449 @@
+# The Lux Philosophy
+
+## In One Sentence
+
+**Make the important things visible.**
+
+## The Three Pillars
+
+Most programming languages hide the things that matter most in production:
+
+1. **What can this code do?** — Side effects are invisible in function signatures
+2. **How does data change over time?** — Schema evolution is a deployment problem, not a language one
+3. **What guarantees does this code provide?** — Properties like idempotency live in comments and hope
+
+Lux makes all three first-class, compiler-checked language features.
+
+---
+
+## Core Principles
+
+### 1. Explicit Over Implicit
+
+Every function signature tells you what it does:
+
+```lux
+fn processOrder(order: Order): Receipt with {Database, Email, Logger}
+```
+
+You don't need to read the body, trace call chains, or check documentation. The signature *is* the documentation. Code review becomes: "should this function really send emails?"
+
+**What this means in practice:**
+- Effects are declared in types, not hidden behind interfaces
+- No dependency injection frameworks — just swap handlers
+- No mocking libraries — test with different effect implementations
+- No "spooky action at a distance" — if a function can fail, its type says so
+
+**How this compares:**
+| Language | Side effects | Lux equivalent |
+|----------|-------------|----------------|
+| JavaScript | Anything, anywhere, silently | `with {Console, Http, File}` |
+| Python | Implicit, discovered by reading code | Effect declarations in signature |
+| Java | Checked exceptions (partial), DI frameworks | Effects + handlers |
+| Go | Return error values (partial) | `with {Fail}` or `Result` |
+| Rust | `unsafe` blocks, `Result`/`Option` | Effects for I/O, Result for values |
+| Haskell | Monad transformers (explicit but heavy) | Effects (explicit and lightweight) |
+| Koka | Algebraic effects (similar) | Same family, more familiar syntax |
+
+### 2. Composition Over Configuration
+
+Things combine naturally without glue code:
+
+```lux
+// Multiple effects compose by listing them
+fn sync(id: UserId): User with {Database, Http, Logger} = ...
+
+// Handlers compose by providing them
+run sync(id) with {
+    Database = postgres(conn),
+    Http = realHttp,
+    Logger = consoleLogger
+}
+```
+
+No monad transformers. No middleware stacks. No factory factories. Effects are sets; they union naturally.
+
+**What this means in practice:**
+- Functions compose with `|>` (pipes)
+- Effects compose by set union
+- Types compose via generics and ADTs
+- Tests compose by handler substitution
+
+### 3. Safety Without Ceremony
+
+The type system catches errors at compile time, but doesn't make you fight it:
+
+```lux
+// Type inference keeps code clean
+let x = 42                    // Int, inferred
+let names = ["Alice", "Bob"]  // List<String>, inferred
+
+// But function signatures are always explicit
+fn greet(name: String): String = "Hello, {name}"
+```
+
+**The balance:**
+- Function signatures: always annotated (documentation + API contract)
+- Local bindings: inferred (reduces noise in implementation)
+- Effects: declared or inferred (explicit at boundaries, lightweight inside)
+- Behavioral properties: opt-in (`is pure`, `is total` — add when valuable)
+
+### 4. Practical Over Academic
+
+Lux borrows from the best of programming language research, but wraps it in familiar syntax:
+
+```lux
+// This is algebraic effects. But it reads like normal code.
+fn main(): Unit with {Console} = {
+    Console.print("What's your name?")
+    let name = Console.readLine()
+    Console.print("Hello, {name}!")
+}
+```
+
+Compare with Haskell's equivalent:
+```haskell
+main :: IO ()
+main = do
+    putStrLn "What's your name?"
+    name <- getLine
+    putStrLn ("Hello, " ++ name ++ "!")
+```
+
+Both are explicit about effects. Lux chooses syntax that reads like imperative code while maintaining the same guarantees.
+
+**What this means in practice:**
+- ML-family semantics, C-family appearance
+- No monads to learn (effects replace them)
+- No category theory prerequisites
+- The learning curve is: functions → types → effects (days, not months)
+
+### 5. One Right Way
+
+Like Go and Python, Lux favors having one obvious way to do things:
+
+- **One formatter** (`lux fmt`) — opinionated, not configurable, ends all style debates
+- **One test framework** (built-in `Test` effect) — no framework shopping
+- **One way to handle effects** — declare, handle, compose
+- **One package manager** (`lux pkg`) — integrated, not bolted on
+
+This is a deliberate rejection of the JavaScript/Ruby approach where every project assembles its own stack from dozens of competing libraries.
+
+### 6. Tools Are Part of the Language
+
+The compiler, linter, formatter, LSP, package manager, and test runner are one thing, not seven:
+
+```bash
+lux fmt        # Format
+lux lint       # Lint (with --explain for education)
+lux check      # Type check + lint
+lux test       # Run tests
+lux compile    # Build a binary
+lux serve      # Serve files
+lux --lsp      # Editor integration
+```
+
+This follows Go's philosophy: a language is its toolchain. The formatter knows the AST. The linter knows the type system. The LSP knows the effects. They're not afterthoughts.
+
+---
+
+## Design Decisions and Their Reasons
+
+### Why algebraic effects instead of monads?
+
+Monads are powerful but have poor ergonomics for composition. Combining `IO`, `State`, and `Error` in Haskell requires monad transformers — a notoriously difficult concept. Effects compose naturally:
+
+```lux
+// Just list the effects you need. No transformers.
+fn app(): Unit with {Console, File, Http, Time} = ...
+```
+
+### Why not just `async/await`?
+
+`async/await` solves one effect (concurrency). Effects solve all of them: I/O, state, randomness, failure, concurrency, logging, databases. One mechanism, universally applicable.
+
+### Why require function type annotations?
+
+Three reasons:
+1. **Documentation**: Every function signature is self-documenting
+2. **Error messages**: Inference failures produce confusing errors; annotations localize them
+3. **API stability**: Changing a function body shouldn't silently change its type
+
+### Why an opinionated formatter?
+
+Style debates waste engineering time. `gofmt` proved that an opinionated, non-configurable formatter eliminates an entire category of bikeshedding. `lux fmt` does the same.
+
+### Why immutable by default?
+
+Mutable state is the root of most concurrency bugs and many logic bugs. Immutability makes code easier to reason about. When you need state, the `State` effect makes it explicit and trackable.
+
+### Why behavioral types?
+
+Properties like "this function is idempotent" or "this function always terminates" are critical for correctness but typically live in comments. Making them part of the type system means:
+- The compiler can verify them (or generate property tests)
+- Callers can require them (`where F is idempotent`)
+- They serve as machine-readable documentation
+
+---
+
+## Comparison with Popular Languages
+
+### JavaScript / TypeScript (SO #1 / #6 by usage)
+
+| Aspect | JavaScript/TypeScript | Lux |
+|--------|----------------------|-----|
+| **Type system** | Optional/gradual (TS) | Required, Hindley-Milner |
+| **Side effects** | Anywhere, implicit | Declared in types |
+| **Testing** | Mock libraries (Jest, etc.) | Swap effect handlers |
+| **Formatting** | Prettier (configurable) | `lux fmt` (opinionated) |
+| **Package management** | npm (massive ecosystem) | `lux pkg` (small ecosystem) |
+| **Paradigm** | Multi-paradigm | Functional-first |
+| **Null safety** | Optional chaining (partial) | `Option<T>`, no null |
+| **Error handling** | try/catch (unchecked) | `Result<T, E>` + `Fail` effect |
+| **Shared** | Familiar syntax, first-class functions, closures, string interpolation |
+
+**What Lux learns from JS/TS:** Familiar syntax matters. String interpolation, arrow functions, and readable code lower the barrier to entry.
+
+**What Lux rejects:** Implicit `any`, unchecked exceptions, the "pick your own adventure" toolchain.
+
+### Python (SO #4 by usage, #1 most desired)
+
+| Aspect | Python | Lux |
+|--------|--------|-----|
+| **Type system** | Optional (type hints) | Required, static |
+| **Side effects** | Implicit | Explicit |
+| **Performance** | Slow (interpreted) | Faster (compiled to C) |
+| **Syntax** | Whitespace-significant | Braces/keywords |
+| **Immutability** | Mutable by default | Immutable by default |
+| **Tooling** | Fragmented (black, ruff, mypy, pytest...) | Unified (`lux` binary) |
+| **Shared** | Clean syntax philosophy, "one way to do it", readability focus |
+
+**What Lux learns from Python:** Readability counts. The Zen of Python's emphasis on one obvious way to do things resonates with Lux's design.
+
+**What Lux rejects:** Dynamic typing, mutable-by-default, fragmented tooling.
+
+### Rust (SO #1 most admired)
+
+| Aspect | Rust | Lux |
+|--------|------|-----|
+| **Memory** | Ownership/borrowing (manual) | Reference counting (automatic) |
+| **Type system** | Traits, generics, lifetimes | ADTs, effects, generics |
+| **Side effects** | Implicit (except `unsafe`) | Explicit (effect system) |
+| **Error handling** | `Result<T, E>` + `?` | `Result<T, E>` + `Fail` effect |
+| **Performance** | Zero-cost, systems-level | Good, not systems-level |
+| **Learning curve** | Steep (ownership) | Moderate (effects) |
+| **Pattern matching** | Excellent, exhaustive | Excellent, exhaustive |
+| **Shared** | ADTs, pattern matching, `Option`/`Result`, no null, immutable by default, strong type system |
+
+**What Lux learns from Rust:** ADTs with exhaustive matching, `Option`/`Result` instead of null/exceptions, excellent error messages, integrated tooling (cargo model).
+
+**What Lux rejects:** Ownership complexity (Lux uses GC/RC instead), lifetimes, `unsafe`.
+
+### Go (SO #13 by usage, #11 most admired)
+
+| Aspect | Go | Lux |
+|--------|-----|-----|
+| **Type system** | Structural, simple | HM inference, ADTs |
+| **Side effects** | Implicit | Explicit |
+| **Error handling** | Multiple returns (`val, err`) | `Result<T, E>` + effects |
+| **Formatting** | `gofmt` (opinionated) | `lux fmt` (opinionated) |
+| **Tooling** | All-in-one (`go` binary) | All-in-one (`lux` binary) |
+| **Concurrency** | Goroutines + channels | `Concurrent` + `Channel` effects |
+| **Generics** | Added late, limited | First-class from day one |
+| **Shared** | Opinionated formatter, unified tooling, practical philosophy |
+
+**What Lux learns from Go:** Unified toolchain, opinionated formatting, simplicity as a feature, fast compilation.
+
+**What Lux rejects:** Verbose error handling (`if err != nil`), no ADTs, no generics (historically), nil.
+
+### Java / C# (SO #7 / #8 by usage)
+
+| Aspect | Java/C# | Lux |
+|--------|---------|-----|
+| **Paradigm** | OOP-first | FP-first |
+| **Effects** | DI frameworks (Spring, etc.) | Language-level effects |
+| **Testing** | Mock frameworks (Mockito, etc.) | Handler swapping |
+| **Null safety** | Nullable (Java), nullable ref types (C#) | `Option<T>` |
+| **Boilerplate** | High (getters, setters, factories) | Low (records, inference) |
+| **Shared** | Static typing, generics, pattern matching (recent), established ecosystems |
+
+**What Lux learns from Java/C#:** Enterprise needs (database effects, HTTP, serialization) matter. Testability is a first-class concern.
+
+**What Lux rejects:** OOP ceremony, DI frameworks, null, boilerplate.
+
+### Haskell / OCaml / Elm (FP family)
+
+| Aspect | Haskell | Elm | Lux |
+|--------|---------|-----|-----|
+| **Effects** | Monads + transformers | Cmd/Sub (Elm Architecture) | Algebraic effects |
+| **Learning curve** | Steep | Moderate | Moderate |
+| **Error messages** | Improving | Excellent | Good (aspiring to Elm-quality) |
+| **Practical focus** | Academic-leaning | Web-focused | General-purpose |
+| **Syntax** | Unique | Unique | Familiar (C-family feel) |
+| **Shared** | Immutability, ADTs, pattern matching, type inference, no null |
+
+**What Lux learns from Haskell:** Effects must be explicit. Types must be powerful. Purity matters.
+
+**What Lux learns from Elm:** Error messages should teach. Tooling should be integrated. Simplicity beats power.
+
+**What Lux rejects (from Haskell):** Monad transformers, academic syntax, steep learning curve.
+
+### Gleam / Elixir (SO #2 / #3 most admired, 2025)
+
+| Aspect | Gleam | Elixir | Lux |
+|--------|-------|--------|-----|
+| **Type system** | Static, HM | Dynamic | Static, HM |
+| **Effects** | No special tracking | Implicit | First-class |
+| **Concurrency** | BEAM (built-in) | BEAM (built-in) | Effect-based |
+| **Error handling** | `Result` | Pattern matching on tuples | `Result` + `Fail` effect |
+| **Shared** | Friendly errors, pipe operator, functional style, immutability |
+
+**What Lux learns from Gleam:** Friendly developer experience, clear error messages, and pragmatic FP resonate with developers.
+
+---
+
+## Tooling Philosophy Audit
+
+### Does the linter follow the philosophy?
+
+**Yes, strongly.** The linter embodies "make the important things visible":
+
+- `could-be-pure`: Nudges users toward declaring purity — making guarantees visible
+- `could-be-total`: Same for termination
+- `unnecessary-effect-decl`: Keeps effect signatures honest — don't claim effects you don't use
+- `unused-variable/import/function`: Keeps code focused — everything visible should be meaningful
+- `single-arm-match` / `manual-map-option`: Teaches idiomatic patterns
+
+The category system (correctness > suspicious > idiom > style > pedantic) reflects the philosophy of being practical, not academic: real bugs are errors, style preferences are opt-in.
+
+### Does the formatter follow the philosophy?
+
+**Yes, with one gap.** The formatter is opinionated and non-configurable, matching the "one right way" principle. It enforces consistent style across all Lux code.
+
+**Gap:** `max_width` and `trailing_commas` are declared in `FormatConfig` but never used. This is harmless but inconsistent — either remove the unused config or implement line wrapping.
+
+### Does the type checker follow the philosophy?
+
+**Yes.** The type checker embodies every core principle:
+- Effects are tracked and verified in function types
+- Behavioral properties are checked where possible
+- Error messages include context and suggestions
+- Type inference reduces ceremony while maintaining safety
+
+---
+
+## What Could Be Improved
+
+### High-value additions (improve experience significantly, low verbosity cost)
+
+1. **Pipe-friendly standard library**
+   - Currently: `List.map(myList, fn(x: Int): Int => x * 2)`
+   - Better: Allow `myList |> List.map(fn(x: Int): Int => x * 2)`
+   - Many languages (Elixir, F#, Gleam) make the pipe operator the primary composition tool. If the first argument of stdlib functions is always the data, pipes become natural. This is a **library convention**, not a language change.
+   - **LLM impact:** Pipe chains are easier for LLMs to generate and read — linear data flow with no nesting.
+   - **Human impact:** Reduces cognitive load. Reading left-to-right matches how humans think about data transformation.
+
+2. **Exhaustive `match` warnings for non-enum types**
+   - The linter warns about `wildcard-on-small-enum`, but could also warn when a match on `Option` or `Result` uses a wildcard instead of handling both cases explicitly.
+   - **Both audiences:** Prevents subtle bugs where new variants are silently caught by `_`.
+
+3. **Error message improvements toward Elm quality**
+   - Current errors show the right information but could be more conversational and suggest fixes more consistently.
+   - Example improvement: When a function is called with wrong argument count, show the expected signature and highlight which argument is wrong.
+   - **LLM impact:** Structured error messages with clear "expected X, got Y" patterns are easier for LLMs to parse and fix.
+   - **Human impact:** Friendly errors reduce frustration, especially for beginners.
+
+4. **`let ... else` for fallible destructuring**
+   - Rust's `let ... else` pattern handles the "unwrap or bail" case elegantly:
+     ```lux
+     let Some(value) = maybeValue else return defaultValue
+     ```
+   - Currently requires a full `match` expression for this common pattern.
+   - **Both audiences:** Reduces boilerplate for the most common Option/Result handling pattern.
+
+5. **Trait/typeclass system for overloading**
+   - Currently `toString`, `==`, and similar operations are built-in. A trait system would let users define their own:
+     ```lux
+     trait Show<T> { fn show(value: T): String }
+     impl Show<User> { fn show(u: User): String = "User({u.name})" }
+     ```
+   - **Note:** This exists partially. Expanding it would enable more generic programming without losing explicitness.
+   - **LLM impact:** Traits provide clear, greppable contracts. LLMs can generate trait impls from examples.
+
+### Medium-value additions (good improvements, some verbosity cost)
+
+6. **Named arguments or builder pattern for records**
+   - When functions take many parameters, the linter already warns at 5+. Named arguments or record-punning would help:
+     ```lux
+     fn createUser({ name, email, age }: UserConfig): User = ...
+     createUser({ name: "Alice", email: "alice@ex.com", age: 30 })
+     ```
+   - **Trade-off:** Adds syntax, but the linter already pushes users toward records for many params.
+
+7. **Async/concurrent effect sugar**
+   - The `Concurrent` effect exists but could benefit from syntactic sugar:
+     ```lux
+     let (a, b) = concurrent {
+         fetch("/api/users"),
+         fetch("/api/posts")
+     }
+     ```
+   - **Trade-off:** Adds syntax, but concurrent code is important enough to warrant it.
+
+8. **Module-level documentation with `///` doc comments**
+   - The `missing-doc-comment` lint exists, but the doc generation system could be enhanced with richer doc comments that include examples, parameter descriptions, and effect documentation.
+   - **LLM impact:** Structured documentation is the single highest-value feature for LLM code understanding.
+
+### Lower-value or risky additions (consider carefully)
+
+9. **Type inference for function return types**
+   - Would reduce ceremony: `fn double(x: Int) = x * 2` instead of `fn double(x: Int): Int = x * 2`
+   - **Risk:** Violates the "function signatures are documentation" principle. A body change could silently change the API. Current approach is the right trade-off.
+
+10. **Operator overloading**
+    - Tempting for numeric types, but quickly leads to the C++ problem where `+` could mean anything.
+    - **Risk:** Violates "make the important things visible" — you can't tell what `a + b` does.
+    - **Better:** Keep operators for built-in numeric types. Use named functions for everything else.
+
+11. **Macros**
+    - Powerful but drastically complicate tooling, error messages, and readability.
+    - **Risk:** Rust's macro system is powerful but produces some of the worst error messages in the language.
+    - **Better:** Solve specific problems with language features (effects, generics) rather than a general metaprogramming escape hatch.
+
+---
+
+## The LLM Perspective
+
+Lux has several properties that make it unusually well-suited for LLM-assisted programming:
+
+1. **Effect signatures are machine-readable contracts.** An LLM reading `fn f(): T with {Database, Logger}` knows exactly what capabilities to provide when generating handler code.
+
+2. **Behavioral properties are verifiable assertions.** `is pure`, `is idempotent` give LLMs clear constraints to check their own output against.
+
+3. **The opinionated formatter eliminates style ambiguity.** LLMs don't need to guess indentation, brace style, or naming conventions — `lux fmt` handles it.
+
+4. **Exhaustive pattern matching forces completeness.** LLMs that generate `match` expressions are reminded by the compiler when they miss cases.
+
+5. **Small, consistent standard library.** `List.map`, `String.split`, `Option.map` — uniform `Module.function` convention is easy to learn from few examples.
+
+6. **Effect-based testing needs no framework knowledge.** An LLM doesn't need to know Jest, pytest, or JUnit — just swap handlers.
+
+**What would help LLMs more:**
+- Structured error output (JSON mode) for programmatic error fixing
+- Example-rich documentation that LLMs can learn patterns from
+- A canonical set of "Lux patterns" (like Go's proverbs) that encode best practices in memorable form
+
+---
+
+## Summary
+
+Lux's philosophy can be compressed to five words: **Make the important things visible.**
+
+This manifests as:
+- **Effects in types** — see what code does
+- **Properties in types** — see what code guarantees
+- **Versions in types** — see how data evolves
+- **One tool for everything** — see how to build
+- **One format for all** — see consistent style
+
+The language is in the sweet spot between Haskell's rigor and Python's practicality, with Go's tooling philosophy and Elm's developer experience aspirations. It doesn't try to be everything — it tries to make the things that matter most in real software visible, composable, and verifiable.
diff --git a/src/main.rs b/src/main.rs
index 23fb476..9090f88 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,4 +1,7 @@
-//! Lux - A functional programming language with first-class effects
+//! Lux — Make the important things visible.
+//!
+//! A functional programming language with first-class effects, schema evolution,
+//! and behavioral types. See `lux philosophy` or docs/PHILOSOPHY.md.
 
 mod analysis;
 mod ast;
@@ -213,12 +216,15 @@ fn main() {
                 // Generate API documentation
                 generate_docs(&args[2..]);
             }
+            "philosophy" => {
+                print_philosophy();
+            }
             cmd => {
                 // Check if it looks like a command typo
                 if !std::path::Path::new(cmd).exists() && !cmd.starts_with('-') && !cmd.contains('.') && !cmd.contains('/') {
                     let known_commands = vec![
                         "fmt", "lint", "test", "watch", "init", "check", "debug",
-                        "pkg", "registry", "serve", "compile", "doc", "repl",
+                        "pkg", "registry", "serve", "compile", "doc", "repl", "philosophy",
                     ];
                     let suggestions = diagnostics::find_similar_names(cmd, known_commands.into_iter(), 2);
                     if !suggestions.is_empty() {
@@ -240,7 +246,12 @@ fn main() {
 
 fn print_help() {
     println!("{}", bc(colors::GREEN, &format!("Lux {}", VERSION)));
-    println!("{}", c(colors::DIM, "A functional language with first-class effects"));
+    println!("{}", c(colors::DIM, "Make the important things visible."));
+    println!();
+    println!("  {} Effects in types — see what code does", c(colors::DIM, "·"));
+    println!("  {} Composition over configuration — no DI frameworks", c(colors::DIM, "·"));
+    println!("  {} Safety without ceremony — inference where it helps", c(colors::DIM, "·"));
+    println!("  {} One right way — opinionated formatter, integrated tools", c(colors::DIM, "·"));
     println!();
     println!("{}", bc("", "Usage:"));
     println!();
@@ -280,6 +291,8 @@ fn print_help() {
         c(colors::DIM, "(alias: s)"));
     println!("  {} {} {}  Generate API documentation",
         bc(colors::CYAN, "lux"), bc(colors::CYAN, "doc"), c(colors::YELLOW, "[file] [-o dir]"));
+    println!("  {} {}           Show language philosophy",
+        bc(colors::CYAN, "lux"), bc(colors::CYAN, "philosophy"));
     println!("  {} {}                Start LSP server",
         bc(colors::CYAN, "lux"), c(colors::YELLOW, "--lsp"));
     println!("  {} {}               Show this help",
@@ -288,6 +301,36 @@ fn print_help() {
         bc(colors::CYAN, "lux"), c(colors::YELLOW, "--version"));
 }
 
+fn print_philosophy() {
+    println!("{}", bc(colors::GREEN, &format!("The Lux Philosophy")));
+    println!();
+    println!("  {}", bc("", "Make the important things visible."));
+    println!();
+    println!("  Most languages hide what matters most in production: what code");
+    println!("  can do, how data changes over time, and what guarantees functions");
+    println!("  provide. Lux makes all three first-class, compiler-checked features.");
+    println!();
+    println!("  {} {}", bc(colors::CYAN, "1. Explicit over implicit"), c(colors::DIM, "— effects in types, not hidden behind interfaces"));
+    println!("     fn processOrder(order: Order): Receipt {} {}", c(colors::YELLOW, "with {Database, Email}"), c(colors::DIM, "// signature IS documentation"));
+    println!();
+    println!("  {} {}", bc(colors::CYAN, "2. Composition over configuration"), c(colors::DIM, "— no DI frameworks, no monad transformers"));
+    println!("     run app() {} {}", c(colors::YELLOW, "with { Database = mock, Http = mock }"), c(colors::DIM, "// swap handlers, not libraries"));
+    println!();
+    println!("  {} {}", bc(colors::CYAN, "3. Safety without ceremony"), c(colors::DIM, "— type inference where it helps, annotations where they document"));
+    println!("     let x = 42                {}", c(colors::DIM, "// inferred"));
+    println!("     fn f(x: Int): Int = x * 2 {}", c(colors::DIM, "// annotated: API contract"));
+    println!();
+    println!("  {} {}", bc(colors::CYAN, "4. Practical over academic"), c(colors::DIM, "— ML semantics in C-family syntax, no monads to learn"));
+    println!("     {} {} {}", c(colors::DIM, "fn main(): Unit"), c(colors::YELLOW, "with {Console}"), c(colors::DIM, "= Console.print(\"Hello!\")"));
+    println!();
+    println!("  {} {}", bc(colors::CYAN, "5. One right way"), c(colors::DIM, "— opinionated formatter, integrated tooling, built-in testing"));
+    println!("     lux fmt | lux lint | lux check | lux test | lux compile");
+    println!();
+    println!("  {} {}", bc(colors::CYAN, "6. Tools are the language"), c(colors::DIM, "— formatter knows the AST, linter knows the types, LSP knows the effects"));
+    println!();
+    println!("  See {} for the full philosophy with language comparisons.", c(colors::CYAN, "docs/PHILOSOPHY.md"));
+}
+
 fn format_files(args: &[String]) {
     use formatter::{format, FormatConfig};
     use std::path::Path;