AbideBotmunu: the language AbideBot 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 psi-terms, and the network that will carry it is designed around hyperbolic routing. Everything on this page is a real excerpt from munu’s source and compiler tests, except two examples written for this page and labelled as such, and anything that says planned.
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.
Contracts and supervision
Recovery rules written as mu-calculus formulas, checked at compile time.
Ports
The one declared place where message order can vary.
Psi-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 AbideBot 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. The syntax is built for that: finite and ongoing functions are told apart up front, functions are tables of cases, and rules come before the body.
nu trigger_loop(state: TriggerState, stream: [OscMessage]) -> [TriggerSnapshot]
step (prev, next) next.generation >= prev.generation
{
_, [] => [],
state, [msg | rest] => {
let it = trigger_step(state, msg);
[it.snap | trigger_loop(it.state, rest)]
},
}State is passed along, not changed
Each message produces a new state, which is handed to the next call as an argument. munu has no mutable variables, loops or compound assignment, so a value on a line is whatever was passed in on that line, and a model never has to replay earlier lines to work out what a variable holds now.
mu values_list_equal(xs: [i64], ys: [i64]) -> bool decreases xs
{
[], [] => true,
[], _ => false,
_, [] => false,
[x | rest_x], [y | rest_y] => if eq_i64(x, y) { values_list_equal(rest_x, rest_y) } else { false }
}Cases on the left, results on the right
Each case pairs a pattern with a result. Calling the function means finding the case whose pattern fits the input and returning the result beside it. That is the shape of attention in a transformer, which compares a query against keys and returns the values paired with the closest matches. The construct munu code is built from is the operation the model is built around.
enum Msg { Buy { sku: string, qty: i64 }, Ping }
mu headline(inbox: [Msg]) -> string {
[Msg::Buy { sku: "tea", qty: 1 } | _] => "1 tea",
[Msg::Buy { sku, .. } | _] => sku,
_ => "nothing"
}One case can look several layers down
Patterns nest. The first case looks into the list, through its first message and down to that message’s fields, testing exact values on the way; the second binds the name sku to the part it needs and skips the rest with ... Because destructuring happens on the left, the result on the right uses those names directly, with no field accesses or chain of conditions, and each case can be as specific a key as it needs to be.
mu is_empty(list: [i64]) -> bool {
[] => true,
[_ | _] => false
}
nu count_from(n: i64) -> [i64] {
n => [n | count_from(n + 1)]
}Finishing or never-ending, declared up front
mu marks a function that must finish: here each case gives its answer at once. nu marks one that never finishes but must keep producing: every step hands back another element before it carries on. Because the keyword comes first, the kind of function is settled before a single case is written.
pub enum FlexDirection { Row, Col }
pub enum FlexJustify { Start, End, Center, SpaceBetween }
pub enum FlexAlign { Start, End, Center, Stretch }
pub enum GridTrack {
Fixed { px: f64 },
Fr { weight: f64 },
Auto,
}Written the way common code is written
Enums, structs, typed fields and braces look the way they do in widely used languages, and list patterns such as [head | tail] follow a long-standing convention. In our measurements 50 of the 54 keywords are single tokens in widely used tokenizers.
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)]
}Requirements, guarantees and the stopping rule come first
What the input must satisfy, what the result promises and why the recursion ends are written before the body, in a fixed order. Writing left to right, a model has read every constraint before it writes the first case.
let bound_var = DataflowVariable { state: 3u64, value: Some(value), ..old_var };
let new_vars = hashmap_insert(dm.variables, canonical_id, bound_var);
let dm2 = DataflowManager { variables: new_vars, ..dm };
let dm3 = match dm2.gc_state {
GcState::RootScan => fold_value_into_marks(value, dm2),
GcState::Transitive => fold_value_into_marks(value, dm2),
GcState::Idle => dm2,
GcState::Sweep => dm2,
GcState::Compact => dm2
};
DmU64 { dm: dm3, val: canonical_id }A record is copied with changes, not edited
The new variable is built from the old one with a few fields replaced (..old_var), and the result is returned as a new value. The match that follows lists all five states with no catch-all case.
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. The None case has no row, so the program is rejected as a non-exhaustive match. With no loop, return, break or try keywords either, every path a function can take is one of its listed cases.
mu f(x: u64) -> u64 { x => { let y: u64; y = x; y } }A name can be declared with its type and no value
From a parser test: a let with a type and no value declares a blank, and the next statement gives it its value. Whatever fills the blank already has a type to fit.
The honest picture: most functions in the source have a single case, and the multi-case tables above are the minority. The mu and nu pair and the deep-pattern example are written for this page; the other excerpts are from munu’s source. The likeness to attention is one of shape only: munu does not compile to attention. 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, and the compiler turns them into checks.
formula permanent() {
nu X. [fail(self, _)] <restart(self)> X and [_] X
}
pub contract Corporal(up_stream: [i64], down_stream: [i64]) -> [u64]
substrate { bytecode }
behaviour { do: permanent() must: permanent() }
{ start_corporal(up_stream, down_stream) }How a bot recovers is written down, not configured
The recovery rule is a mu-calculus formula: on any failure, restart, and keep doing that for as long as the component runs. Each component names its rule in its header (do: is what it does, must: is what it is held to), and the compiler turns the formula into a state machine at build time.
pub contract Supervisor(x: u64) -> [u64]
substrate { bytecode }
behaviour {
do: nu X. [fail(left, Failure::Lost)] <restart(left)> X
and [done(left)] <absorb(left)> X
and [_] X
must: nu X. [fail(!self, _)]~deadline(RESPONSE_MUST) X
}
children { left: Worker }Different failures get different answers
A supervisor lists its children and answers each kind of failure on its own line: restart the child on one cause, absorb a child that has finished, and be held to answering a child’s failure within a stated deadline. This is from a compiler test, which also checks the other side: an answer to a failure the child can never raise is refused at compile time, so there is no dead recovery code.
pub enum FetchFailure { EndedWithoutObject }
pub mu first_object(objects: [u64]) -> u64 {
[] => crash FetchFailure::EndedWithoutObject,
[object | rest] => object
}A failure has a name and a type
Failures are declared like any other type and raised with crash. The reason travels to the supervisor, which is what lets recovery rules match on the cause instead of on a log line.
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) }Deadlines sit next to the logic they cover
Each component states a target time and a hard limit for its steps (~deadline). The limits are declared as named constants, so the numbers you hold a bot to live in the same file as the code that has to meet them.
Excerpts are unedited apart from indentation, with one exception noted in the second row: the compiler test fills in the failure name.
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.
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
}The one declared place where order can vary
A port is where several senders feed one stream. It names its ends, a bound on how many values can wait, and a formula for the orders it accepts: here neither sensor may speak until the controller has, after which anything goes, within the stated deadlines. Every other value in the language has a single writer, so the system is designed so that run-to-run variation can enter only through ports like this one, and everything else can be reproduced.
Shared work, filled in by many.
munu’s types are 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}) -> u64 { r => 0u64 }
mu g(r: {a: bool}) -> u64 { r => 0u64 }
mu main() -> u64 { _ => { let y; let z = 1u64; let r = {a: y}; f(r); g(r) } }
mu main() -> u64 { _ => { let y; let r; r = {a: y}; r = {a: 1i64}; 0u64 } }Shared work that several parties fill in
Types are psi-terms: structures that can be partly known. A record can be built with a blank field (let y;), and each part of the program that uses it adds what it knows about that field, checked against what the others said. In the first compiler test one call expects a number and the other a true-or-false value, so the program is refused. In the second, a later assignment fills the blank. This is designed for bots collaborating on shared work: each adds what it knows, and a conflict is caught instead of overwritten.
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
An app draws itself by returning a scene: a tree of layout, text and controls built by ordinary mu functions. Nothing is painted until munuScene reads the tree. Because the screen is data, munuScene is designed to hand the same tree to the agent, which can read it and 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
let click; declares a variable with no value yet. The button is wired to it, and pressing it fills it in, once. The stream returns the current scene and then hands the variable to the next step, which continues only when the variable has a value. There are no callbacks or handlers to register: a party that needs a fact waits on its variable, and a party that knows it binds it.
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
Long-term memory is declared as relations with keys and typed fields, and changed only through transaction blocks that assert or retract facts. The compiler stops a query from calling a transaction, so reading memory can never change it.
query snapshot(target: string, t: i64) -> [string] {
target, t => as_of(t) {
let _ <- Dep { from: name, to: target, .. };
name
}
}Ask what was true at a point in time
A query can run as_of an earlier moment, or ask for everything since one, which is designed for audits and incident reviews: what did the bot know when it acted?
Excerpts are unedited apart from indentation.
A network with no central directory.
The routing code is written in munu and exists today. The global network that will use it, connecting every munuOS machine and every bot by its QR code with end-to-end encryption, is planned.
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
Each node is given coordinates in the Poincaré disk, a model of hyperbolic space, and this function measures the distance between two of them. A packet goes to whichever neighbour is closest to its destination, so a node needs to know only its neighbours, not the whole network. Hyperbolic space has room for very large trees with short paths, which is why it is used for routing.
pub contract HyperbolicRouting() -> [RoutingEvent]
substrate { bytecode }
behaviour {
do:
nu X.
[from(self)]
<to(self)> true
and [_] X
must: true
}
{ hyperbolic_routing_loop() }The router is held to a rule as well
The router is a contract like any other part. Its formula says that at every step, whenever something arrives, sending it on must stay possible. The same supervision and checking that apply to your code apply to the parts of the system that move it.
Excerpts are unedited apart from one internal comment removed from the contract header.
Three parts, one language.
How AbideBot 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 Planned
Shared state as psi-terms in one store, designed so tells commute and only the new part of a value travels. Routed by hyperbolic coordinates and encrypted end to end. Sites, documents and apps are designed to live here, not on the public web.
The honest picture: the compiler, the code shown above and munuOS’s first stages exist. The agent’s direct use of apps in munuScene, the network, 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@abidebot.com.