# Atlas

> Atlas reads code (Python, TypeScript, Rust) into a small piece of mathematics and draws it: types are objects, functions are arrows between them, a program is what composing those arrows gives, and every place where data rests (a file, a table, a URL, the screen, a module's global) is part of the arrows that reach it. The picture is a proof, not an illustration: every box and arrow is derived from the code, nothing is guessed. A human and a coding agent share it, so that pointing at a box and saying "this should not exist" is a statement both can act on.

## Read this first: Atlas lays problems bare, it does not solve them

Agents who work on or with Atlas tend to make one mistake, and it is the mistake that matters most. When a picture looks wrong, the reflex is to make Atlas read the code better: a special case, a regex over strings, a table entry for one project, a heuristic that guesses what the author meant. With Atlas that reflex is the error.

- **When the picture looks wrong, first ask whether the code says what is missing.** If it does not, because a type is not annotated, a path is looked up by a key at run time, or a call goes through a dictionary, then the gap in the picture is the finding. Atlas draws it as a gap: a place the code does not name, a call it cannot follow, a step without a type. The code is what should change.
- **Never add a rule to Atlas so a picture looks the way someone expects.** An expected picture is no target. A rule that only fits one project, one library call or one picture is a hack. The engine knows languages and libraries, never a project.
- **Only what can be traced exists.** A difference between careful and careless code is real for Atlas only if some fact in the graph differs. Where a language lets the careless form say exactly what the careful one says, Atlas shows nothing, and that is correct. Where a language forbids the careless form (Rust's signatures are always typed), there is nothing to lay bare.
- **When Atlas does misread clean code, fix Atlas, generally.** Settle "Atlas or the code?" with a pair: the same program written as good practice has it and with the usual shortcut. The careful side must read as the mathematics says; the careless side must show as careless, never as clean and never not at all. The pairs live in `engine/tests/pairs`.
- **A finding is a question for the author, not an error to suppress.** Atlas coaches; it does not fix.

## What Atlas is

Atlas is a metalanguage above programming languages: a proof machine whose proofs are pictures. The principles are stated once, on the graph, for every language. A new language brings a reader, never a principle. The same program written in Python, TypeScript and Rust gives the same picture where the languages agree, so a port can be checked against its original. Where the pictures differ, the languages differ.

The mathematics:

- **Category theory gives the structure** ([an introduction](https://pttrn.io/#content/category-theory)). Types are objects and functions are arrows. Call order is composition, and a route is a composite from an entry point to the places it reaches. Zooming out is a quotient (a family of types becomes one box); keeping to one route, one package or one kind of edge is a fiber. The two don't commute, so the order of a view is meaning.
- **Topology gives the zoom.** A zoom level divides the nodes into boxes: a partition, and so a topology on them. Zooming out glues a family into one point (a quotient), zooming in refines it; the levels are ordered from fine to coarse as topologies are, so the picture stays the same picture.
- **Graph theory gives the routes.** A route is what an entry point reaches; a step's own arrow and everything it reaches are different quantities and are never merged.
- **Effects are part of a function's type, as in a type-and-effect system.** A function's domain is its parameters plus what it reads; its codomain is what it returns plus what it writes, sends or runs.
- **What Atlas checks are the laws of that structure.** A sum type is a coproduct, taken apart where it arises. A class that writes a place and reads it back is a lens, and a lawful one at the level of types: what it puts as `A` it gets back as `A` (put-get). An override keeps its base's promise (behavioural subtyping, Liskov). A function whose value is used says what it gives.

The mathematics is there so that a human needs none of it. Every construct has one shape and every program is drawn by the same rules, so a person sees at a glance whether a picture is consistent. Keep it that way: a special case in the engine is a shape that means something else in one place, and it breaks exactly that.

## Using Atlas as an agent

- `atlas check [repo] --json` lists where the code and the eleven principles disagree.
- `atlas revelation [repo] --json` lists the prophecies in the tree: sketch code marked as not built yet (`@prophecy(supersedes=..)` in Python, `#[doc = "prophecy: .."]` in Rust, `@prophecy` in a TypeScript JSDoc), what each supersedes and what is left to build. A prophecy can be `sealed="#144"` on an open question: `seals` lists them with the state of the issue (via `gh`), `unseal` breaks them (named, or all whose issue is closed). `prophetize` decides your `vision`: it writes its files into the tree with the added items marked, and leaves them for the person to commit. `check` asks about built code that leans on one.
- `atlas changes [rev]` says what an edit did to the routes, their places and the findings. Run it after an edit to see whether the edit did what it was meant to, and nothing else.
- `atlas mcp` serves the same over stdio: the tools `principles`, `check`, `revelation`, `explain`, `routes`, `route`, `choices`, `view` and `changes`. `choices` lists the choices a route makes, each with what decides each branch as the code writes it and what each branch runs: read the conditions and say what they mean, Atlas does not. It is registered once for every project: `claude mcp add --scope user atlas -- atlas mcp` in Claude Code, `codex mcp add atlas -- "$(command -v atlas)" mcp` in Codex (which starts servers without the shell's `PATH`). It works on the repository the agent runs in.
- **`atlas serve` is where the person you work with looks at the code.** Their page and you share one view through `atlas mcp`: `shown` says what they have open (read it when they say "this box" or "here"), `look` takes their page to a view or points at a box or a line ("look here, this one"), `vision` draws a change you plan beside the code as it is (give the files it would write as sketch code: signatures, types and calls in order, bodies left empty; it has to parse, not to build), so you ask "shall I do this?" with a picture rather than in words, then `retract` it once decided, `annotate` puts your own words on a box or a line (what a condition of `choices` means, what a step is for), and `notes` lists what they wrote on boxes and lines, each with a link to its place. Handle a note in your own reply, by a fix or by explaining (Atlas is no chat), then `resolve` it, with the commit if one fixed it; reading a note does not resolve it. A note worth keeping (a real bug) goes into an issue with its link; give the issue to `resolve`. The page follows the code: what you edit is drawn anew in the view they have, a moment after you save. If they are not running it, suggest `atlas serve` in the repository.
- `atlas view [repo]` writes the same picture as one HTML file, an export: in `.atlas/` at the top of the git repository unless `--out` names a place (MCP `view` takes `out`). Use it to hand over a picture when no `atlas serve` runs: open that file for them or give it to them. The folder ignores itself, so git never sees it.
- **Porting a program to another language** (or checking someone's port): draw the original and the port, and compare their routes (`atlas mcp`'s `route`, or the two pictures). A faithful port draws the same shape: the same steps in the same order, the same values handed between them, the same places. Every difference is either drift, which the port should fix (a step folded into `main`, a file picked inside a function, a global that was not there), or the language, which you name (a pandas `DataFrame` becomes a `Vec<Month>`, a function that may fail says so with `Result`). Tests show the output survived; the picture shows the design did.

## Docs

- [Design](https://raw.githubusercontent.com/raoulg/atlas/main/docs/reference/design.md): the shared language, the algebra, how each language is read, and the views. Start with §0.
- [Mathematics](https://raw.githubusercontent.com/raoulg/atlas/main/docs/reference/mathematics.md): every mathematical notion Atlas uses, once, with what it is in Atlas and where it lives.
- [Principles](https://raw.githubusercontent.com/raoulg/atlas/main/docs/reference/principles.md): the eleven principles `atlas check` asks, each with its reasoning and idioms, and a table of what each language lets Atlas trace.
- [Guide](https://raw.githubusercontent.com/raoulg/atlas/main/docs/reference/guide.md): how to read the picture, what Atlas reads in each language, entry points, `check`, `changes` and the MCP tools.

## Optional

- [The pairs](https://github.com/raoulg/atlas/tree/main/engine/tests/pairs): programs written carefully and carelessly, and the tests that state what Atlas shows of each. The sunspot pipeline (`pairs/pipeline`) is one program written as a sloppy script, typed Python, TypeScript and Rust.
- [The showcase](https://raoulg.github.io/atlas/): the same pictures, for people.
- [README](https://raw.githubusercontent.com/raoulg/atlas/main/README.md)