# Muro

> Muro is an explicit affine dependent type theory built for agents to write: the agent writes the program together with its types, motives and proofs, nothing is inferred, and `mix muro.check` accepts or rejects every definition. Definitions are tagged `spec`, `evidence` or `run`; a spec never becomes evidence and evidence never becomes a run. Proofs are erased, and only `run` terms are emitted. The default emitter is Elixir. `--backend c` writes C, `--backend rust` writes Rust, `--backend zig` writes Zig, `--backend asm` writes Cortex-M assembly, and `--backend otp` writes a GenServer for a session. `--backend fsm` prints each session endpoint as a state machine. `--backend exunit` prints an ExUnit suite for the book's closed equations. A closed `Nat` run is also a NIF. `--node` writes one call for a cross. Agda specifies the calculus and proves the checker sound on a fragment. Agda does not check the `.muro` file.

Nothing is inferred: there are no implicits, unification, metavariables or tactics, and every binder and motive is written out. A `?` always fails. Recursion in `run`, `evidence`, and `spec` must descend. Agents should read the For agents page first, and copy syntax from the files in `examples/` rather than writing it from memory. `out of fuel` is not acceptance; raise `--fuel` and check again.

## Docs

- [Manual](https://muro-lang.dev/docs): What Muro is, how to read this book, and the three documentation layers.
- [For agents](https://muro-lang.dev/docs/for-agents): Two jobs. Do not mix them. Commands and file map.
- [Start](https://muro-lang.dev/docs/start): Install, write a .muro file, check it, emit Elixir.
- [Marks](https://muro-lang.dev/docs/marks): Π, λ, modes, data, atoms, and streams, one paragraph each.
- [The wall](https://muro-lang.dev/docs/wall): spec, evidence, and run. Promotion is forbidden.
- [Terms](https://muro-lang.dev/docs/language): Type, Π, λ, match, quantities, and the book.
- [Sessions](https://muro-lang.dev/docs/sessions): A session is the protocol two processes follow.
- [Grammar](https://muro-lang.dev/docs/grammar): The surface grammar lib/muro/parser.ex implements.
- [Identity](https://muro-lang.dev/docs/identity): Equations, refl, rewrite, and explicit motives.
- [Data](https://muro-lang.dev/docs/data): Inductive types, positivity, Maybe, List, Tree.
- [Indexed data](https://muro-lang.dev/docs/indexed): Fin, Vec, and lookup without a runtime bounds check.
- [Streams](https://muro-lang.dev/docs/streams): ν, unfold, Always, and bisimulation.
- [Either and Dec](https://muro-lang.dev/docs/either): Disjoint union and decisions. Not LEM.
- [Machine numbers](https://muro-lang.dev/docs/machine): I64, F32, Tensor, and Nx. Nat stays Peano.
- [Emit](https://muro-lang.dev/docs/emit): What becomes Elixir. C, Rust, and Zig print the closed run. A Nat run is a NIF. Cortex-M prints a Nat run. OTP writes a conforming process. A session endpoint is a state machine. A cross is one call on a named node. Spec and evidence are omitted from a run.
- [State machines](https://muro-lang.dev/docs/fsm): Each session endpoint is a pure state machine. The transport stays with the host.
- [Closed equations as tests](https://muro-lang.dev/docs/exunit): A book's closed equations become one ExUnit module. The tests call an implementation the host names. A skip is printed and recorded.
- [Mutation](https://muro-lang.dev/docs/mutate): `mix muro.mutate` reports which evidence fails when a `run` definition changes.
- [Visual explorer](https://muro-lang.dev/docs/explorer): `muro_visor` draws a checked book. `muro ui path.muro` prints how to install it. The compiler does not start the explorer.
- [Committed modules](https://muro-lang.dev/docs/gen): A manifest names each book, module, and target. `mix muro.gen` writes the module. `mix muro.gen --check` fails when the file and the book disagree.
- [The executable](https://muro-lang.dev/docs/binary): The self-contained `muro` binary, `muro.toml`, gen for C, Rust, Zig, and assembly, init, and `muro skills add`.
- [Host representations](https://muro-lang.dev/docs/repr): A repr states the host shape of a data type. Emit writes strict decode and encode. Decode returns `{:ok, value, table}`. Encode takes that table.
- [Packages](https://muro-lang.dev/docs/packages): Import a book from a git or Hex package at the version `muro.lock` records. `mix muro.deps.get` fetches `muro_deps/` and writes the lock.
- [Library](https://muro-lang.dev/docs/library): The ordinary library, imported as `std:`. Bool, Le, List, Maybe, and comparison.
- [Limits](https://muro-lang.dev/docs/limits): What the language does not do. Facts about the checker, not a roadmap.

## Examples

- [Examples](https://muro-lang.dev/docs/examples): Every file in examples/ and what it is for.
- [half_ok.muro](https://github.com/murolang/muro/blob/main/examples/half_ok.muro): The canonical book: a spec, a program, and a theorem about it.
- [examples/ on GitHub](https://github.com/murolang/muro/tree/main/examples): All example programs.

## Repository

- [murolang/muro](https://github.com/murolang/muro): Source, README, CI (Elixir tests and `make agda`).
- [muro on Hex](https://hex.pm/packages/muro): The Mix package; check files with `mix muro.check`.
- Archive: `mix muro.check`, `mix muro.mutate`, `mix muro.emit`, `mix muro.gen`, `mix muro.init`, and `mix muro.deps.get` in any directory. Install with `mix archive.install hex muro`. A pinned version: `mix archive.install hex muro 0.20.7`. From a checkout: `mix archive.build && mix archive.install muro-0.20.7.ez`. From GitHub: `mix archive.install github murolang/muro` (fetches the default branch and builds it). A project without Elixir installs the self-contained executable: `mise use -g github:murolang/muro@0.20.7`. It carries its own Erlang runtime. `muro check`, `muro emit`, and `muro gen` match the Mix tasks. The manifest without Mix is `muro.toml`. Inside a project that depends on muro, the project's copy runs after `app.start`. Inside any other project, or outside a project, the archive's copy runs and the host is neither compiled nor started. `mix muro --version` prints the copy that ran. `mix run --no-start` does not see the archive: archives are on the code path only for Mix tasks. `mix muro.mutate path.muro` reports which evidence fails when a `run` definition changes. `mix muro.emit path.muro` prints the Elixir module. `mix muro.emit path.muro --backend fsm` prints one state machine per session. `mix muro.emit path.muro --backend exunit` prints the suite, including a library of unsupplied `param`s. `--imports` with that backend also collects the book's direct imports. `mix muro.gen` writes the modules named by `muro.exs` (or a `:muro` key in `mix.exs`). `mix muro.gen --check` fails when a committed module and its book disagree. `mix muro.init` creates the manifest and `priv/muro/`. `mix muro.deps.get` fetches `muro_deps/` and writes `muro.lock`. `mix muro.check` on a book that imports packages prints one `conforms to` line per package.

## Optional

- [Extending the kernel](https://muro-lang.dev/docs/extending): How to change the type theory. Agda first, then Elixir.
- [CSHRL](https://muro-lang.dev/docs/cshrl): Coinductive symmetric homomorphisms for RL, as a library on params, with three environments and their agents.
- [CHANGELOG](https://github.com/murolang/muro/blob/main/CHANGELOG.md): Release history.