munu: the language munubot is written in.
munu is a programming language for programs that have to keep running and be checked before they do. Functions are finite (mu) or ongoing (nu). Programs are contracts that carry their own recovery rules and deadlines. Shared state is single-assignment dataflow over ψ-terms (psi-terms), and the network that carries it is in development, built on hyperbolic routing and encrypted frames. Everything on this page is a real excerpt from munu’s source and compiler tests, except seven examples written for this page and labelled as such and anything that says planned.
Dotted terms show their meaning on hover or focus, and all of them are in the glossary.
The munu source, docs and tooling are not public yet. They are planned to open with the beta, around February 2027.
mu and nu
Finite functions and ongoing streams, told apart by their first word, in a syntax shaped for a transformer.
Contracts and supervision
Recovery rules written as mu-calculus formulas, checked at compile time.
Ports
The one declared place where message order can vary.
ψ-terms
Shared structures that several parties fill in, with conflicts caught.
Dataflow and scenes
Every variable is set once, and code waits until it has a value. An app’s screen is ordinary data that both you and your agent can read.
Facts and history
Typed facts, transactions, and queries as of a past moment.
Hyperbolic routing
Greedy routing on a curved map, for a network with no central directory.
munuOS, munuScene, network
How the three parts of munubot fit around munu.
Shaped for the model that writes it.
munu is designed to be written mostly by an AI agent and read by people, and its syntax is shaped around how a transformer works. Each example shows what its code does, then why the feature suits a model that writes it.
Why it suits a model
A model writes code one token at a time from the text it can see; it cannot run the program, watch it, or remember what happened last time.
munu is built for that.
Whether a function ends is its first word, whether work runs or waits is written on its declaration, and the one place order can vary is a declared port, so every question a model would otherwise have to simulate is answered on the page.
Every variable is set once, so a name means the same thing wherever it appears, and recovery rules and deadlines sit in the contract’s header instead of in config somewhere else.
When something is wrong, the compiler says which line and what to change, so the model’s next edit is already written.
And models working together
Models cooperate by filling the same variables, not by sending each other messages.
Agents read and set the same dataflow variables. A model writes no networking, sync, retry or locking code, and a remote variable reads just like a local one. Each variable is set only once, and every message travels sealed in an encrypted frame, so what arrives is what was sent.
As models specialise, some will hold data most people shouldn’t read, such as a hospital’s clinical model. So access to a variable is designed as a capability the program carries, not a policy stored somewhere else. In our tests between node processes, capabilities already guard connections and port sends.
mu add(total: i64, n: i64) -> i64 {
total, n => total + n
}
mu tally() -> i64 {
_ => {
let s1 = add(0, 2);
let s2 = add(s1, 3);
add(s2, 4)
}
}State is passed along, not changed
tally never changes a value: add takes the running total and returns the next one, and each result is handed on by name, s1 into the call that makes s2. A transformer’s context window holds only the text in front of it, and here that text is everything a step depends on: add(s1, 3) names its whole input, with no field changed somewhere else for the model to keep track of. So each call can be written or checked from the tokens right beside it.
Try: change add(s1, 3) to add(s2, 3) and press Run. It is refused (UndefinedVariable): undefined variable `s2`
, with did you mean: `s1`?
enum Light { Red, Amber, Green }
mu can_go(light: Light, emergency: bool) -> bool {
_, true => true,
Light::Green, false => true,
Light::Amber, false => false,
Light::Red, false => false
}+1 hidden line
Added after it, to run it:
mu run() -> bool { _ => can_go(Light::Green, false) }
Cases on the left, results on the right
Each row of can_go is a pattern on the left and a result on the right, and the first row that fits is taken. That is the shape of attention, the core step of a transformer, which matches a query against keys to pick out their values: here the inputs are the query, each pattern is a key and each result is its value. Every row is short and repeats the shape of the one above, so the model writes and checks it from the tokens on that line, and the compiler rejects a missing row or one that can never match.
Try: copy the Light::Green, false => true, row so that it appears twice and press Run. It is refused (UnreachableArm): this arm can never match: the arms of `can_go` above it without a `when` guard already match every value it matches -- remove it, or move it above the arm that takes its values
struct Item { sku: string, qty: i64 }
enum Msg { Buy { item: Item }, Ping }
mu headline(inbox: [Msg]) -> string {
[Msg::Buy { item: Item { sku: "tea", qty: 1 } } | _] => "1 tea",
[Msg::Buy { item: Item { sku, .. } } | _] => sku,
_ => "nothing"
}+1 hidden line
Added after it, to run it:
mu run() -> string { _ => headline([Msg::Buy { item: Item { sku: "tea", qty: 1 } }]) }
One case can look several layers down
headline reads the first message of an inbox: a Buy of one tea gives "1 tea", any other Buy gives its sku, bound three levels down with the rest skipped by .., and anything else gives "nothing". Each pattern repeats the shape of the types declared just above it, Msg and Item, so the model writes it by copying a shape that is already in its context. The result then uses sku directly, with no chain of field accesses that could name the wrong field.
Try: change qty: 1 to qty: 2 in the first pattern and press Run. That pattern no longer fits the message, so the second one answers and the result changes from “1 tea” to “tea”.
mu is_empty(list: [i64]) -> bool {
[] => true,
[_ | _] => false
}
nu count_from(n: i64) -> [i64] {
n => [n | count_from(n + 1)]
}+1 hidden line
Added after it, to run it:
mu run() -> bool { _ => is_empty([]) }
Finishing or never-ending, declared up front
mu marks a function that must finish, like is_empty, which answers at once; nu marks one that never finishes but must keep producing, like count_from, which hands back another element before it carries on. The keyword is the first token of the declaration and a model generates left to right, so everything it writes after it is conditioned on the kind of function it has already committed to. The kind is never left for the body to reveal.
Try: change nu count_from to mu count_from and press Run. It is refused (NuCanon): recursive mu `count_from` missing decreases clause
enum Size { Small, Large }
struct Cup { size: Size, price: i64 }
mu first_price(cups: [Cup]) -> i64 {
[] => 0,
[head | _] => match head.size {
Size::Small => head.price,
Size::Large => head.price + 1
}
}+1 hidden line
Added after it, to run it:
mu run() -> i64 { _ => first_price([Cup { size: Size::Large, price: 3 }]) }
Written the way common code is written
first_price returns the first cup’s price, plus one if the cup is Large, and 0 for an empty list. Enums, structs, braces and match are written as they are in widely used languages, and the list pattern [head | _] follows a long-standing convention, so much of this is a shape the model has seen many times and can continue token by token. In our measurements 50 of the 54 keywords are single tokens in widely used tokenizers, so the keywords mostly reach the model whole.
Try: change Size::Large in the second arm to Size::Huge and press Run. It is refused (UndefinedVariant): undefined variant `Huge` on enum `Size`
mu ring_truncate(list: [Histogram], k: i64) -> [Histogram]
requires (k >= 0i64)
ensures (r) hist_list_len(r) <= k
decreases list
{
[], _ => [],
[_ | _], 0i64 => [],
[head | tail], k => [head | ring_truncate(tail, k - 1i64)]
}+8 hidden lines
Added before the code shown:
struct Histogram { n: i64 }
mu hist_list_len(list: [Histogram]) -> i64
decreases list
{
[] => 0i64,
[_ | tail] => 1i64 + hist_list_len(tail)
}
Requirements, guarantees and the stopping rule come first
ring_truncate states what its input must satisfy (requires), what the result promises (ensures) and why the recursion ends (decreases), and only then gives its three cases. A model writes left to right, so by the first case every constraint is already in its context and each token of the body is generated with them in view. The order is fixed, so each kind of rule is always found in the same place.
Try: delete the decreases list line and press Check. It is refused (NuCanon): recursive mu `ring_truncate` missing decreases clause
struct Account { owner: string, balance: i64 }
mu deposit(a: Account, n: i64) -> Account {
a, n => Account { balance: a.balance + n, ..a }
}+1 hidden line
Added after it, to run it:
mu run() -> i64 { _ => deposit(Account { owner: "you", balance: 10 }, 2).balance }
A value is copied with changes, not edited
deposit returns a new Account with the balance replaced, and ..a fills in every other field from the original, which is left as it was. A model works out what a name holds by attending back to the text that made it. Since nothing is edited in place, that text stays true for the rest of the program, so what the model read for a earlier is still what a is where it is used.
Try: delete , ..a and press Run. It is refused (MissingStructField): missing field `owner` on `Account`
pub enum Event {
Click { name: string },
None,
}
mu handle(e: Event) -> i64 {
Event::Click { name } => 1i64,
}A missing case is a compile error
This is from a compiler test. handle has a row for Click but none for None, so the program is rejected as a non-exhaustive match, where a failure found only at run time would leave nothing to read.
The compiler says: the arms of `handle` do not match every value of its parameter, of type `Event`: no arm matches `Event::None` -- add an arm that matches it, or end with a catch-all arm `_ => ...`; an arm with a `when` guard does not count, and literals never cover an integer or string type
It names the missing case and gives two ways out, so the model’s next edit is already written.
Try: add Event::None => 0i64, under the first row and press Check. It now passes.
mu one_thing() -> i64 {
_ => {
type P;
let x;
let y: P;
x: P;
x = y;
P = i64;
y = 42;
x
}
}A name can be declared with its type and no value
x and y start with no value, and x = y joins them into one variable before either has one; P = i64 then fixes their shared type, and y = 42 gives that one variable its value, so x reads 42. Every = in munu is a bind, and once two things are joined they stay one thing. A model goes only by the text, so what x is gets answered by the lines that bind it, not by working out when each line ran.
Try: change P = i64; to P = bool; and press Run. It is refused (ConstraintFailure): `y` has type `bool` and is given a value of type `42..=42`, but a variable keeps one type -- make the two agree
mu add(a: i64, b: i64) -> i64 {
a, b => a + b
}
mu square(n: i64) -> i64 {
n => n * n
}
mu meet() -> i64 {
_ => {
let x;
let y;
let total = spawn add(x, y);
x = spawn square(3);
y = spawn square(4);
total
}
}Spawned work meets in a variable
meet declares x and y with no value, spawns add(x, y) before either has one, and only then binds them to square(3) and square(4), so total is 9 + 16 = 25. The variable is the unit of concurrency: spawn hands back the variable a result will be bound to and has no say over when a call runs, which the function’s declaration settles; add waits only where it reads x or y while they are unbound, and every variable is bound once, so the answer is the same in any order. A model sees only text, never timing, and here every dependency is a named variable in the text, so it can reason about the values on the page and not about an interleaving it cannot observe.
Try: move the let total line below the two binds and press Run. The value stays 25 and the step count drops from 8 to 6.
lazy mu share(n: i64) -> i64 {
n => 100 / n
}
mu only_what_is_read() -> i64 {
_ => {
let a = spawn share(4);
let b = spawn share(0);
a
}
}Work happens only when its result is needed
only_what_is_read spawns share(4) and share(0) but returns only a, so it gives 100 / 4 = 25. share is declared lazy mu, so a call runs its body only when something reads its variable: nothing reads b, so 100 / 0 never runs, and spawn has no say in that, because the declaration settles it. Laziness is written once on the declaration, never at the call, so the model can tell from the text which work runs and which waits until it is read, without simulating an evaluation order it cannot observe.
Try: delete lazy and press Run. The program crashes with DivideByZero, even though b is never read.
The honest picture: most functions in munu’s source have a single case, and multi-case tables like those above are the minority. The short examples on this page (passed-along state, the table, deep patterns, mu and nu, familiar forms, a copied value, the joined names, the spawned consumer and the lazy calls) are written for it; the others are from munu’s source. The fit with a transformer is a design rationale and a likeness of shape only: munu does not compile to attention, and we have not measured that it lowers error rates. Effects such as receiving a message happen through calls, not through syntax. In our own tests the language is not more compact than mainstream languages. Its advantage is structure, not size.
Recovery is part of the program.
A contract is munu’s unit of work, supervision and security. How it recovers and how fast it must answer are written as mu-calculus formulas and constants in the code, so they sit in the text the model is writing, and the compiler turns them into checks.
pub contract Ward() -> [u64]
substrate { bytecode }
behaviour {
do: nu X. [fail(patient, Failure::Wounded)] <absorb(patient)> X and [_] X
must: true
}
children { patient: Medic }
ports {
reports: [Report] {
ends: a
bound: REPORTS_BOUND
do: nu X. [_] X
must: true
}
}
{
let self.patient = spawn Medic(BED, reports.a);
collect(reports, ONE)
}+32 hidden lines
Added before the code shown:
module page_recovery
enum Failure { Wounded }
enum Report { Reading(u64), ChildFailed(u64, u64), ChildDone(u64) }
const REPORTS_BOUND = 8u64;
const BED = 1u64;
const ONE = 1u64;
cdf RESPONSE {
dmax: 200ms,
handup: 50ms,
expected: [(10ms, 0.9), (50ms, 0.99), (200ms, 1.0)]
}
eager nu attend(id: u64, out: [Report].end) -> [u64] {
id, out => {
let _ = send(out, Report::Reading(id));
crash Failure::Wounded
}
}
pub contract Medic(id: u64, out: [Report].end) -> [u64]
substrate { bytecode }
{ attend(id, out) }
eager nu collect(rs: [Report], left: u64) -> [u64] {
_, 0u64 => [],
[], _ => [],
[r | rest], left => match r {
Report::Reading(id) => [id | collect(rest, left - 1u64)]
}
}
Recovery is written beside the code, so the build can check it
Ward absorbs its medic’s failure in do:, but its must: is true, so it promises no response time, and a contract that answers a child’s failure on a port has to state one. The build refuses it, points at the must: line and says what to add, which a model can act on directly. The rule and its deadline are one header, checked before the bot runs. Written for this page.
The compiler says: contract `Ward` receives child failures on a port, so its must line needs the time it may take to answer any child failure, and it gives none -- add `[fail(!self, _)]~deadline(D)` to the must line, with D a declared cdf or a duration such as 5ms
It names the line and the exact text to add, so the model’s next edit is a copy from the message.
Try: change the must: true line under behaviour to must: nu X. [fail(!self, _)]~deadline(RESPONSE) X and press Check. It now passes. RESPONSE is a cdf with several points: 90% of answers within 10ms, 99% within 50ms and every one within 200ms.
enum Failure { Lost, Wounded }
enum Report { Reading(u64), ChildFailed(u64, u64), ChildDone(u64) }
const REPORTS_BOUND = 8u64;
const ALPHA = 1u64;
const BRAVO = 2u64;
cdf RESPONSE {
dmax: 200ms,
handup: 50ms,
expected: [(10ms, 0.9), (50ms, 0.99), (200ms, 1.0)]
}
eager nu drill(id: u64, out: [Report].end) -> [u64] {
id, out when id == ALPHA => {
let _ = send(out, Report::Reading(id));
crash Failure::Lost
},
id, out => {
let _ = send(out, Report::Reading(id));
crash Failure::Wounded
}
}
pub contract Corporal(id: u64, out: [Report].end) -> [u64]
substrate { bytecode }
{ drill(id, out) }
eager nu command(rs: [Report]) -> [u64] {
[] => [],
[r | rest] => match r {
Report::Reading(id) => [id | command(rest)]
}
}
pub contract Major() -> [u64]
substrate { bytecode }
behaviour {
do: nu X. [fail(alpha, Failure::Lost)] <restart(alpha)> X
and [fail(bravo, Failure::Wounded)] <absorb(bravo)> X
and [_] X
must: nu X. [fail(!self, _)]~deadline(RESPONSE) X
}
children { alpha: Corporal, bravo: Corporal }
ports {
reports: [Report] {
ends: a, b
bound: REPORTS_BOUND
do: nu X. [_] X
must: true
}
}
{
let self.alpha = spawn Corporal(ALPHA, reports.a);
let self.bravo = spawn Corporal(BRAVO, reports.b);
command(reports)
}+1 hidden line
Added before the code shown:
module page_supervision
A major restarts one corporal and absorbs the other’s failure
Major starts two corporals that each send a reading and crash, and its do: answers each failure by its own rule: restart(alpha) for Failure::Lost and absorb(bravo) for Failure::Wounded. So the readings begin 1, 2 and then keep giving 1 as alpha restarts, until the step limit on this page stops the run, while absorbing bravo lets Major carry on without it. Each rule is one line, a failure on the left and its answer on the right, the same repeating shape as the cases of a function, so a model continues it row by row. Written for this page.
Try: change restart(alpha) to absorb(alpha) and press Run. Nothing starts alpha again, so the run stops after the first two readings, 1 and 2, with “Stopped: nothing left could make progress”.
pub enum FetchFailure { EndedWithoutObject }
pub mu first_object(objects: [u64]) -> u64 {
[] => crash FetchFailure::EndedWithoutObject,
[object | rest] => object
}+2 hidden lines
Added before the code shown:
module page_failures
Added after it, to run it:
mu run() -> u64 { _ => first_object([7u64]) }
A failure has a name and a type
first_object crashes with FetchFailure::EndedWithoutObject when the stream ends before an object arrives. A failure is a declared type and crash carries it to the supervisor, so recovery rules match on the cause, not on a log line. For a model that works from text, a declared name is a precise token to match on, where free-form message text would have to be interpreted.
Try: change FetchFailure::EndedWithoutObject in the crash line to FetchFailure::Missing and press Run. It is refused (CrashReasonNotAVariant): the crash reason `FetchFailure::Missing` is no variant of an enum in scope -- write a unit variant of an enum declared in this module or imported with `use`, as in `crash Failure::Lost` for `enum Failure { Lost }`
cdf FETCH_DO = 2s
cdf FETCH_MUST = 30s
pub contract Fetcher(anchor_key: u64, commitment: string, size: i64) -> [u64]
substrate { bytecode }
behaviour {
do: nu X. [_]~deadline(FETCH_DO) X
must: nu X. [_]~deadline(FETCH_MUST) X
}
{ fetch_and_arrive(anchor_key, commitment, size) }+3 hidden lines
Added before the code shown:
nu fetch_and_arrive(anchor_key: u64, commitment: string, size: i64) -> [u64] {
anchor_key, commitment, size => [anchor_key | fetch_and_arrive(anchor_key, commitment, size)]
}
Deadlines sit next to the logic they cover
Fetcher gives its steps a do: and a must: deadline, FETCH_DO (2s) and FETCH_MUST (30s), written as named cdf constants and applied with ~deadline. A model cannot observe how long anything takes, only the text, so a time limit it can read and write beside the logic it covers is one it can work with. Here each is a single time; the recovery row above uses a cdf with several points.
Try: change FETCH_MUST in the must: line to FETCH_SLOW and press Check. It is refused (ContractDelayUnresolved): contract `Fetcher` writes ~deadline(FETCH_SLOW) in its must, and `FETCH_SLOW` is no cdf declared in this module, so the deadline would be lost -- declare `FETCH_SLOW` as a cdf in this module, or name a cdf it declares
Excerpts are unedited apart from indentation. The second row is written for this page, following the shapes in the compiler’s tests.
The only place order can vary.
Every other value in munu has a single writer. Where several senders must feed one stream, you declare a port and say which orders it accepts, so the one place order can vary is written in the text.
pub contract SensorHub() -> [u64]
substrate { bytecode }
behaviour { do: nu X. [_] X must: true }
children { controller: Source, left: Source, right: Source }
ports {
readings: [Reading] {
ends: ctl, lhs, rhs
bound: READINGS_BOUND
do:
[from(lhs)] false
and [from(rhs)] false
and [from(ctl)] nu X. [_] X
must:
<from(ctl)>~deadline(CONFIG_MUST) true
and nu X. [_]~deadline(SAMPLE_MUST) X
}
}
{
let self.right = spawn Source(RIGHT_CHANNEL, readings.rhs);
let self.left = spawn Source(LEFT_CHANNEL, readings.lhs);
let self.controller = spawn Source(CONTROL_CHANNEL, readings.ctl);
take(readings, COUNT)
}+42 hidden lines
Added before the code shown:
module page_ports
const READINGS_BOUND = 8u64;
const LEFT_CHANNEL = 1u64;
const RIGHT_CHANNEL = 2u64;
const CONTROL_CHANNEL = 0u64;
const COUNT = 3u64;
cdf CONFIG_MUST {
dmax: 20ms,
handup: 5ms,
expected: [(1ms, 0.9), (5ms, 0.99), (20ms, 1.0)]
}
cdf SAMPLE_MUST {
dmax: 200ms,
handup: 50ms,
expected: [(10ms, 0.9), (50ms, 0.99), (200ms, 1.0)]
}
struct Reading { channel: u64, value: u64 }
nu idle(r: Reading) -> [Reading] {
r => [r | idle(r)]
}
eager nu speak(channel: u64, out: [Reading].end) -> [Reading] {
channel, out => {
let r = Reading { channel: channel, value: channel };
let _ = send(out, r);
[r | idle(r)]
}
}
pub contract Source(channel: u64, out: [Reading].end) -> [Reading]
substrate { bytecode }
{ speak(channel, out) }
eager nu take(rs: [Reading], left: u64) -> [u64] {
_, 0u64 => [],
[], _ => [],
[r | rest], left => [r.channel | take(rest, left - 1u64)]
}
The only place non-determinism can enter
SensorHub starts three sources that feed one port, readings, and its formula says neither sensor may speak until the controller has, so the readings begin with the controller and then 2 and 1 in an order the contract leaves open; CONFIG_MUST and SAMPLE_MUST, each a cdf with several points, say how soon each must arrive. The port is the only source of non-determinism in munu, since every other value has one writer, so a failure that varies from run to run has one place to look. A model sees text and never timing, and the contract names the rule to tighten. Written for this page.
Try: move the left spawn line above the right one and press Run. The readings change from [0, 2, 1] to [0, 1, 2]: the controller is still first, as the formula requires.
Shared work, filled in by many.
munu’s types are ψ-terms (psi-terms): structures that can be partly known. Each party adds what it knows, and the store checks it against what everyone else said.
mu f(r: {a: i64}) -> i64 {
r => 0
}
mu g(r: {a: bool}) -> i64 {
r => 0
}
mu main() -> i64 {
_ => {
let y;
let r = {a: y};
f(r);
g(r)
}
}mu read_a(r: {a: i64}) -> i64 {
{a: x} => x
}
mu main() -> i64 {
_ => {
let y;
let r;
r = {a: y};
let seen = spawn read_a(r);
r = {a: 1};
seen
}
}Shared work that several parties fill in
In the first block f needs y to be a number and g needs it to be true or false, so the build refuses it, because a variable keeps one type. In the second, r starts as {a: y} with the blank still open, so the spawned read_a asks for a before anyone has told it, waits, and gets 1 once the other statement fills the blank, whatever the line order. A model writes left to right and often does not yet know every field, so a blank lets it leave a field open and fill it in later instead of inventing a placeholder. Written for this page.
The compiler says: `r` has type `{a: i64}` and is given a value of type `{a: bool}`, but a variable keeps one type -- make the two agree
It names the variable and both types, so the model knows which side to change.
Try: in the first block change bool in g to i64 and press Check: it passes, because both functions agree about the field. In the second, move r = {a: 1}; above the spawn line and press Run: it still gives 1, because the reader now finds the field already filled.
Variables that are filled once, and screens that are data.
A munu variable starts empty, is filled in once and is never changed. Anything that needs it waits until it has a value. Apps use the same rule for input, and draw themselves as scene values.
mu button_face(label: string) -> SceneNode {
label => SceneNode::Layout {
node: LayoutNode::Styled {
fill_color_r: 0.18, fill_color_g: 0.42, fill_color_b: 0.55, fill_color_a: 1.0,
child: pad(16.0, 32.0, 16.0, 32.0, text(label))
}
}
}A screen is a value
button_face returns a scene: a styled layout with a fill colour and padding around the label’s text, built by ordinary mu functions, and nothing is painted until munuScene reads the tree. A screen that is a value is text a model can read and write, which a screen of pixels is not, and munuScene is designed to hand the same tree to the agent so it can act on it without a screenshot.
eager nu click_cycle(n: u64) -> [SceneNode] {
n => {
let click;
let label = if n == 0u64 { "Click me" } else { "Clicked!" };
let scene = pad(40.0, 40.0, 40.0, 40.0,
click_surface(click, button_face(label)));
[scene | wait_click(n, click)]
}
}Wait for a value to be bound
click_cycle returns the current scene, then waits on click, a variable with no value yet that the button fills in once; the next step continues only when it has one. There are no callbacks or handlers to register. A model sees only text, so a wait that is one named variable in the code, with the button wired to it beside it, is a dependency it can read directly instead of tracing to a handler elsewhere.
From a test program in munu’s source. munuScene, the browser, is in development, and the agent reading scenes and binding their variables is designed, not shipped.
Memory you can question later.
Long-term memory is a set of typed facts, changed only in transactions and queried as of any moment.
pub relation Module { name: string @key, path: string, lines: i64 }
pub transaction add_module(name: string, path: string, lines: i64) -> () {
name, path, lines => {
assert Module { name: name, path: path, lines: lines };
}
}Memory is a set of typed facts
Module is a relation with a key and typed fields, and memory is changed only through transactions like add_module, which assert a fact. The compiler stops a query from calling a transaction, so reading memory can never change it. The keyword that opens each piece of code, query or transaction, tells a model from the text whether it can change memory, and a mix-up is rejected with a message it can read.
Try: add query peek(name: string) -> () { name => { add_module(name, "x", 0) } } at the end and press Check. It is refused (CallingConventionViolation): query `peek` cannot call transaction `add_module`
query snapshot(target: string, t: i64) -> [string] {
target, t => as_of(t) {
let _ <- Dep { from: name, to: target, .. };
name
}
}+1 hidden line
Added before the code shown:
relation Dep { from: string, to: string }
Ask what was true at a point in time
snapshot runs as_of(t) and lists the names that depend on target at time t; a query can also ask for everything since a moment, which is designed for audits and incident reviews. The moment is written inside the query, on the same line as the question, so a model writing or reviewing it finds the time it asks about in the query’s text, not in a log or setting elsewhere.
Try: change to: target to into: target and press Check. It is refused (RecordPatternFieldNotFound): field `into` not found on relation `Dep`, whose fields are `from`, `to`
Excerpts are unedited apart from indentation.
A network with no central directory.
The routing code is written in munu and runs today between separate node processes in our tests, with every message sealed in an encrypted frame. Joining every munuOS machine and every bot, reachable by its QR code, is still ahead.
Records in the middle
IP moves packets to places, and named-data networking moves data by name. munu moves structured data that is still being worked out, so ψ-terms (psi-terms) sit in the middle. You can send a record before you know all of it, and anyone reading a field that is missing just waits until someone fills it in. A reader asks and the owner tells; nothing is pushed unasked.
Every field has exactly one writer. If a node tells something that contradicts what is already there, that thread is refused and fails, and the data stays as it was.
Underneath, each node has a place on the hyperbolic map and forwards by distance, and every message travels in a fixed-size BlackFrame, sealed end to end and again hop by hop with X25519 and ChaCha20-Poly1305, so a forwarder sees only where a frame is going.
Built and tested between node processes: the routing, the frames, refused contradictions and waiting readers. Still ahead: sending partial records over the wire (closed values and streams cross today), and linking munuOS machines.
use remote::*;
const FORCE_READ = 0u64;
pub mu consume(anchor_key: u64, contract_key: u64, expected_bytes: u64) -> u64 {
anchor_key, contract_key, expected_bytes => {
let lifted = lift(anchor_key, contract_key, expected_bytes);
lifted + FORCE_READ
}
}A variable that lives on another node
lift turns another node’s address into a variable, and adding to it is the read: the read demands the value, the variable waits until the owner tells it, and only then does the sum resolve.
A remote variable is read like a local one, so a model writes one pattern, with no locks, retries or sync code, and the waiting sits in the variable instead of in the program. That suits a model that writes left to right and cannot see what else is running. This comes from the network tests, which run separate node processes on localhost; munuOS machines are not linked yet, and the browser runs a single kernel, so it is an excerpt you cannot run here.
mu hyperbolic_distance(r1: f64, a1: f64, r2: f64, a2: f64) -> f64 {
r1, a1, r2, a2 => {
let x1 = f64_mul(r1, f64_cos(a1));
let y1 = f64_mul(r1, f64_sin(a1));
let x2 = f64_mul(r2, f64_cos(a2));
let y2 = f64_mul(r2, f64_sin(a2));
let dx = f64_sub(x1, x2);
let dy = f64_sub(y1, y2);
let delta_sq = f64_add(f64_mul(dx, dx), f64_mul(dy, dy));
let d1sq = f64_sub(1.0, f64_mul(r1, r1));
let d2sq = f64_sub(1.0, f64_mul(r2, r2));
let denom = f64_mul(d1sq, d2sq);
f64_acosh(f64_add(1.0, f64_div(f64_mul(2.0, delta_sq), denom)))
}
}Every node has a place on a curved map
hyperbolic_distance measures how far apart two nodes are in the Poincaré disk, each given as a radius and an angle; a packet goes to the neighbour closest to its destination by this measure, so a node needs to know only its neighbours. The body names every intermediate value on its own line, x1, dx, delta_sq, denom, and each is bound once. So each line is written from names directly above it, a nearby, explicit dependency of the kind a transformer works from.
pub contract HyperbolicRouting() -> [RoutingEvent]
substrate { bytecode }
behaviour {
do:
nu X.
[from(self)]
<to(self)> true
and [_] X
must: true
}
{ hyperbolic_routing_loop() }+5 hidden lines
Added before the code shown:
enum RoutingEvent { Arrived }
nu hyperbolic_routing_loop() -> [RoutingEvent] {
_ => [RoutingEvent::Arrived | hyperbolic_routing_loop()]
}
The router is held to a rule as well
HyperbolicRouting is a contract like any other part: its do: formula says that whenever something arrives (from(self)), sending it on (to(self)) must stay possible. It uses the same header syntax as the contracts above, so a model that has written one contract header repeats the same shape for the router, and the same supervision and checking apply.
Try: change <to(self)> to <to(nobody)> and press Check. It is refused (UnknownFormulaAddress): unknown formula address: `nobody` names nothing this formula may address; the names it may use are `self`
Excerpts are unedited apart from one internal comment removed from the contract header and the comments removed from the two remote-variable functions.
Terms used on this page.
- cdf
- A cumulative distribution function: a deadline written as several points, such as 90% within 10ms, 99% within 50ms and all within 200ms, instead of one number.
- contract
- A declaration around a function whose rules are checked when it is built: how it answers its children’s failures (do:), what it promises (must:) and which ports it listens on.
- deterministic
- The same program gives the same answer however its parts are scheduled, except where a port lets the order of messages vary.
- lazy
- A function declared lazy runs its body only when something reads its result; the choice is made once on the function, not at each call.
- mu
- A function that must finish: it returns a value, and a recursive one has to show with a decreases clause that it ends.
- mu-calculus
- A small logic for rules about what happens over time; the do: and must: lines of a contract are formulas in it.
- nu
- A function that never has to finish but must keep producing: each turn hands back another element.
- ψ-term (psi-term)
- A record that can be partly known: a field may be left blank and filled in once, and a fill that contradicts what is there is refused.
- port
- The declared place where several senders feed one stream, and so the only place message order can vary.
- spawn
- Starts a call and hands back the variable its result will be bound to; it has no say over when the call runs, which the function’s declaration settles.
- supervision
- A parent contract starting child parts and saying, for each failure, how it answers, for example restart the child or absorb the failure.
- variable
- A name that starts empty and is bound once; anything that reads it waits until it has a value, which makes the variable the unit of concurrency.
Three parts, one language.
How munubot is put together around munu. Parts marked planned or in development are designs, not shipped software.
munuOS In development
The always-on operating system the agent lives in: a minimal Linux-based operating system image where munu is the first process, one per customer. It includes the munu compiler. It is designed so the agent writes a module, compiles it on munuOS and swaps it in, with supervision restarting a failed part by its rule and a bad version rolling back.
munuScene In development
The AI-native browser and desktop app. It draws scenes, not HTML, and turns what you press and type into values bound to the variables the app is waiting on. The agent runs on munuOS, not in munuScene, and is designed to use the same scenes as you do.
The network In development
Shared state as ψ-terms in one store, designed so tells commute and only the new part of a value travels. Routed by hyperbolic coordinates, with every message sealed in an encrypted BlackFrame. The routing and the frames are built and tested between nodes; running it between munuOS machines is planned. Sites, documents and apps are designed to live here, not on the public web.
The honest picture: the compiler, the code shown above, the routing and encrypted frames between test nodes, and munuOS’s first stages exist. The agent’s direct use of apps in munuScene, the network between munuOS machines, self-hosting and published docs are planned. We will not claim savings or uptime before we can measure them.
Build on munu.
The beta is planned for around February 2027, for developers and munu enthusiasts. Join the waitlist on the home page, or write to us at hello@munubot.com.