Introduction: There Is No Send

What Osmol Is

Osmol is not a language for telling computers what to do. It is a language for declaring what is true about a participant (what they hold, seek, owe, decide, permit, and protect), so that a mesh of such declarations can be continuously solved for equilibrium. An Osmol program never executes in the imperative sense. It settles, the way a spreadsheet settles after a cell changes, or the way water settles between connected tanks.

Every earlier communication technology shipped with a language built from envelopes: objects "send messages," processes have "mailboxes," APIs "post" and "push." Osmol is the first grammar in which the act of sending is not discouraged, not deprecated, but unwritable. There is no construct that transmits content to a party. Instead, each participant compiles to a twin, a machine-readable state of assertions (hold), gaps (seek), commitments (owe), and decisions (decide), wrapped in a permission membrane and defended by an attention budget. When one twin holds what another twin seeks, and the holder's membrane permits it, and the resulting pressure clears the threshold of the receiver, then knowledge flows. Communication is what settling looks like from the inside.

There is no send.

Fifty-Five Years of Envelopes

Already in 1971, Ray Tomlinson sent a message from one computer to another on ARPANET and chose the @ symbol to separate the person from the machine. He could not later remember what the first message said. This is fitting: the medium was never designed to care what you said. It was designed to make sure the saying arrived.

That was the correct problem for 1971. Claude Shannon had established in 1948 that the engineering of communication could, and should, set meaning aside entirely; the job was to move symbols across a channel with fidelity. Email is the purest civilian descendant of that idea. It standardized transport and deliberately refused to standardize meaning. Every email is, to the network, an opaque blob addressed to a mailbox; a human on the far end supplies all understanding. For half a century this was wisdom, because humans were the only readers in existence. The assumption quietly expired in the mid-2020s, when the receiving end of a message stopped needing to be a human mind.

And there is a detail from 1971 that reads today like prophecy. In the same year email was born, the economist Herbert Simon published his diagnosis of information-rich societies: that information consumes the attention of its recipients, and hence, in his words, "a wealth of information creates a poverty of attention." So the disease and its cause were born in the same year. Email prices attention at zero. An inbox is the only to-do list in your life that any stranger on Earth may write on, without permission, at no cost. Spam and reply-all storms are not abuses of that system; they are rational responses to a broken price signal. Every self-declared email killer (the chat apps, the team rooms) attacked the client and inherited the disease, adding inboxes instead of removing one. It took fifty-five years before the symptoms became unbearable. Osmol is a grammar written for the year they did.

From Seven Laws to Five Axioms

The Fifty-Year Letter, the manifesto from which Osmol grew, distills what communication in 2026 must become into Seven Laws: Receiver Sovereignty (attention belongs to the person receiving), Declared Intent (every communication object states what it is), Compiled State (threads are source code; the build artifact is a queryable ledger of decisions and commitments), Layered Actors (agents exchange logistics so humans can exchange meaning), Proven Provenance (authorship is a cryptographic claim), Adaptive Fidelity (author once, render per receiver), and Open Protocol (federated, or failed). Osmol is those laws made into grammar. The Five Axioms (there is no send; programs are claims, not commands; the receiver's grammar governs; precision only flows downhill; the human lane is verbatim) are the load-bearing translation of the laws into syntax, and everything else in this book derives from them.

Where Osmol Stands Today

This book is honest about size, so we settle first the claims before making new ones.

Status, plainly stated.

• What exists: a v0.1 language specification; a single-file Python reference interpreter, published on PyPI as osmol 0.1.0, whose documented pragmas are normative for v0.1 behavior (see The v0.1 Pragmas); and Theorem 1 (Convergence), machine-checked in Coq with zero axioms, but over an abstracted membrane oracle, meaning the proof covers the flow bookkeeping, not the pressure arithmetic (see Theorem 1).
• What does not exist yet: Theorems 2-5 are open. No network transport exists. The wire protocol is specified on paper only, and every mesh that has ever settled did so inside one process. The conformance suite is a plan with two seed programs. There are zero users.

The right metaphor is a blueprint and a working model train versus an actual railroad. Most blueprints never become railroads. The ones that do start exactly like this, and starting does not guarantee becoming.

If that paragraph made you more interested rather than less, you are this book's reader.

How This Book Is Organized

The book is written for an engineer who wants to implement Osmol in any language. The specification and the machine-checked theorems define the language; this book is how you pick them up and carry them.

• The Tutorial installs the reference interpreter and walks the canonical two-twin dinner mesh from source to settled trace, ending with the one thing the machine refuses to do for you (resolving decides).
• The Reference specifies every construct, the grammar, and also every diagnostic (because in this language the error messages are the ethics), including the sentences that cannot be written.
• Semantics gives the pressure function, the granularity lattice, the equilibrium model, and the proof: what is machine-checked, what is open, and exactly where the line between them sits.
• Carrying the Stone is the part for implementers: the normative pragmas of the reference interpreter, the conformance suite, and the road from one process to a real wire.
• Community covers governance, the RFC process, and how the language versions. This is installed now, at population one, because governance retrofitted after adoption is how open protocols quietly become products.

Osmol is MIT-licensed, copyright 2026 The Osmol Language Contributors. The stone is public, versioned, and governed; what it is not, yet, is carried far. That is what the rest of this book is for.

Installation

Osmol v0.1 ships as a reference interpreter: one Python file, osmol.py, published on PyPI as the osmol package. Installing takes about one minute, and at the end of this page you will have run the toolchain and downloaded the two canonical example programs.

Requirements

• Python 3.9 or newer. The interpreter uses only the standard library: no dependencies, no build step, no compiler.
• Also a terminal. That is the whole list.

The entire v0.1 implementation is a single file. If you are here to implement Osmol in another language, that file is also your most compact executable reading of the semantics. See The Reference Interpreter and The v0.1 Pragmas.

Install from PyPI

pip install osmol

If you prefer isolated tool installs, pipx works too:

pipx install osmol

Both install version 0.1.0, the current release.

Windows note

On Windows, Python from the Microsoft Store does not put installed console scripts on your PATH, so a bare osmol command may not be found even though the package installed correctly. For that reason, the canonical invocation everywhere in this book is:

python3 -m osmol

This form works on every platform and every Python install, so this is what we standardize on. On macOS and Linux (and on Windows installs where the scripts directory is on PATH), you may use osmol directly and substitute it in your head throughout.

Verify

Run the interpreter's help:

python3 -m osmol --help

You should see:

usage: osmol.py [-h] [--resolve twin:fact=value] file

Osmol v0.1 reference interpreter

positional arguments:
  file

options:
  -h, --help            show this help message and exit
  --resolve twin:fact=value
                        inject a human judgment for a pending decide

That is the entire command-line surface of v0.1: a file to settle, and --resolve for injecting human judgments into pending decide declarations. (Why judgments must be injected rather than computed is a load-bearing design decision, see Resolving Decides.)

Get the example programs

Two programs ship with the language and anchor its conformance story:

• dinner.osmol: the two-twin mesh from spec §8 (maya and raj coordinating dinner), which settles to equilibrium in three flows. You will spend the next two chapters inside it.
• spam.osmol: a one-line program that dies at parse time with error[O-000], demonstrating that in Osmol, spam is a syntax error.

Download them from the official repository:

curl -O https://raw.githubusercontent.com/osmol-lang/osmol/main/dinner.osmol
curl -O https://raw.githubusercontent.com/osmol-lang/osmol/main/spam.osmol

(curl is built into Windows 10 and later, macOS, and most Linux distributions. You can also download the files by hand from github.com/osmol-lang/osmol.)

A quick taste of what you just fetched. This is spam.osmol in its entirety:

twin spammer {
  send offer(crypto) to everyone
}

Try running it. The interpreter will refuse, loudly, before any semantics happen. That refusal is the founding gesture of the language: there is no send.

You're done when

python3 -m osmol --help prints the usage text above, and dinner.osmol and spam.osmol sit in your working directory. Then continue to Your First Twin.

Your First Twin

In this chapter you will write the smallest Osmol program that does anything: two twins, one fact, one gap, and a single flow between them. Along the way you meet most of the moving parts of the language, and you notice also the one part that never appears.

If you have not installed the interpreter yet, start with Installation.

A program with no main

An Osmol program has no entry point, because nothing in it executes. Axiom II of the specification says it plainly: programs are claims, not commands. Every statement is a declarative speech act: an assertion, a gap, a commitment, a decision, an expression, or a permission. There are no loops, no sequencing, no control flow, and the order of declarations never matters.

This takes a moment to trust. In every language you have used, line 3 runs before line 4. In Osmol, line 3 and line 4 are both simply true, the way two rows of a database are both true. You can shuffle every declaration in the program of this chapter and the result will not change by one character. The program does not run; it settles. The mesh solves the declared state for equilibrium, the way water finds one level across connected tanks.

So instead of asking "what does this program do?", we ask the Osmol question: what does each participant claim, and what follows from those claims together?

The smallest mesh that flows

Save this as first.osmol:

-- first.osmol — the smallest mesh that flows
twin ana {
  hold weather(berlin) = rainy
  bond ben { trust high }

  membrane {
    weather(*) -> family: exact
  }
}

twin ben {
  seek weather(berlin)
  bond ana { trust high }
}

Five constructs, each with a full reference page in Part II:

• twin blocks are the compilation unit, one per participant. Everything a twin declares is about itself; the grammar cannot say anything about the insides of anyone else.
• hold is an assertion: ana claims she possesses a value for the fact weather(berlin). Assertions are the mesh's supply side.
• seek is a gap: a first-class record that ben lacks this value and has standing interest in it. Gaps are the demand side, and the only thing that can attract flow. This one has no deadline, so it simply stands.
• membrane is ana's permission layer. The rule weather(*) -> family: exact says: facts matching weather(*) may reach my family circle at full precision. In v0.1, family means any party the sender bonds with trust high, which is why ana bonds ben.
• bond declares trust. Ben's bond toward ana does two things on his side: it sets the trust weight of anything arriving from her, and it classifies her as family for his attention threshold (default 0.3, see The Pressure Function).

Notice what ben did not write. He never named ana as the source of the weather. He declared an absence, and that is all.

Run it

$ python3 -m osmol first.osmol
OSMOL v0.1 - reference interpreter
parsed first.osmol: 2 twins, 0 sends (no such construct exists)
initial gapcount: 1   (Theorem 1 bound: equilibrium in <= 1 flows)
t1  ana.weather(berlin) --exact--> ben   P=1.00 (R1.0*U1.0*T1.0*M1.0) > theta[family]=0.3   [silent]

EQUILIBRIUM after 1 flows (Theorem 1 bound 1: respected)
messages composed by humans: 0 (the grammar has no verb for it)
interruptions: 0
open gaps: 0 — silence is a fixpoint

Read the trace from the top. The header counts one open gap in the whole mesh, and Theorem 1 (machine-checked) guarantees equilibrium within that many flows. The interpreter asserts this bound at runtime.

The t1 line is a flow firing, with its full pressure arithmetic printed: relevance R, urgency U, trust T, and membrane cast M multiply to a pressure of 1.00, which clears ben's family-class threshold of 0.3. The membrane cast was exact, so ben now holds weather(berlin) = rainy at full precision. The placement is [silent]: ben's twin simply knows now; nothing renders, nothing buzzes. Reading the Trace walks every field in detail.

Then the footer: equilibrium, zero human messages, zero interruptions, zero open gaps. Silence is a fixpoint.

Remove the membrane rule

Delete ana's membrane block entirely and run again:

initial gapcount: 1   (Theorem 1 bound: equilibrium in <= 1 flows)

EQUILIBRIUM after 0 flows (Theorem 1 bound 1: respected)
messages composed by humans: 0 (the grammar has no verb for it)
interruptions: 0
open gap [ben]: weather(berlin)

No flow. Ben's gap stays open, and the mesh reports it honestly at the footer.

This is the protective default of v0.1, visible in the source of the interpreter: when no membrane rule matches a fact, membrane_cast returns None, and no rule means no flow. Nothing ana holds can leave her twin unless a rule of hers grants passage, and nothing arrives at ben that no permission produced. Silence is not an error state here; it is the correct equilibrium of these particular claims. If you want the flow back, ana must say so in her own grammar.

What you did not write

Look back at first.osmol and count the absences.

You wrote no send. There is no such verb; try one and you get error[O-000] before anything else is even parsed.

Also no address. Ben never routed a request to ana; he declared a gap, and the mesh found the holder who was willing.

And no schedule: no polling loop, no retry logic, no delivery callback. The pressure function evaluated, one flow fired, and the mesh settled.

Two twins declared what was true about themselves, and communication happened as a consequence, that is, as the resolution of pressure between declared states. That is the whole language, in miniature. The next chapter, The Dinner Mesh, scales this up to the canonical two-twin program with deadlines, commitments, a human decision, and the human lane.

The Dinner Mesh

Every language has one program that everyone knows. C has hello, world. Osmol has the dinner mesh: two people, one evening, one overdue code review, and not a single message. This is dinner.osmol, the canonical program that ships with the reference interpreter, and at the end of this chapter you will be able to read every line of it the way the equilibrium engine does.

Here it is, exactly as it lives in the osmol repository:

-- dinner.osmol — the Spec §8 mesh, now runnable
twin maya {
  hold eta(dinner) = 19:40 ±5m, decays 20:00
  seek venue(dinner) by 18:00 else escalate
  owe review(atlas) to raj by fri
  bond raj { trust high }
  express to raj: "Saw a fox on the way home and thought of you."

  membrane {
    eta(*) -> family: exact
    eta(*) -> others: coarse(30m)
    status(*) -> team: category
  }
  attention {
    interrupts 2/day
    quiet 22:00-07:00
    threshold others 0.8
  }
}

twin raj {
  decide venue(dinner) among { verde, banh-mi-house } by 18:00
  seek eta(dinner) by 19:00
  seek status(atlas.review) by thu else sync
  bond maya { trust high }

  membrane {
    venue(*) -> family: exact
    decision(*) -> family: exact
  }
  attention {
    interrupts 4/day
  }
}

Note: this file differs deliberately from spec §8. The program in the specification is the idealized dinner mesh; this one is the runnable one. Three additions and one omission. It adds bond raj { trust high } to maya (so the two twins are in each other's inner circle in both directions), it adds the express (so you can watch the human lane deliver), and it adds a venue(*) membrane rule to raj, because when raj's decision resolves, the assertion it emits is named venue(dinner), and without a matching rule the answer could never cross his membrane. It omits assume role reviewer(atlas), because the v0.1 interpreter does not parse assume role (see the v0.1 pragmas). Everything else is spec §8, character for character.

Maya, line by line

hold eta(dinner) = 19:40 ±5m, decays 20:00 is an assertion, the supply side of the mesh. Maya's twin claims a value: her ETA is 19:40, with ±5m of honest uncertainty, because she is a person crossing a city, not a train timetable. The decays 20:00 clause is temporal validity: once dinner has really started, an ETA is trivia, and the claim expires on its own. Nobody has to remember to un-say it. The full type of this assertion is a triple, (instant, exact, decays 20:00), because in Osmol, time and precision are part of the type, not metadata.

seek venue(dinner) by 18:00 else escalate is a gap, the demand side, and the only thing in the entire language that can attract flow. Maya does not know where dinner is. She does not ask anyone; she declares the absence. The by 18:00 deadline gives the gap urgency, and else escalate says: as the deadline nears, raise the priority of this gap rather than letting it lapse.

owe review(atlas) to raj by fri is a commitment. Maya owes raj the atlas review by Friday. Commitments generate structural supply automatically: in v0.1 this line also emits hold status(atlas.review) = in-progress on maya's side, because an unmet promise implies the standing interest of the counterparty in its status. Maya never has to write "just an update, still working on it" again. The owe is the update.

bond raj { trust high } is a bond. Raj is inner-circle. In v0.1, this is also what makes raj count as family when maya's membrane speaks of audiences (the circles pragma: family and team match any party the sender bonds trust high; others is everyone else).

express to raj: "Saw a fox on the way home and thought of you." is the human lane. This is the only place in Osmol where free prose may appear, and it crosses the mesh verbatim, provenance-labeled, untouched by any membrane transform or attention rule. The fox is not information. The fox is the point.

The membrane contains three permission rules, typed as casts. Family sees maya's ETA exact; everyone else sees it rounded to coarse(30m); her team sees the status of her work at category grain, that is in progress, not the details. Notice what the membrane cannot say: there is no rule that sharpens. Precision only flows downhill (Axiom IV, see the five axioms).

The attention block is maya's sovereign budget. Two interruptions a day, quiet from 22:00 to 07:00, and a threshold of 0.8 for strangers. These numbers are legal only inside maya's own twin; no other program on Earth can reference, lower, or spend them (Axiom III).

Raj, line by line

decide venue(dinner) among { verde, banh-mi-house } by 18:00 is an open decision. Two options, one deadline. A decide generates gaps for its unevaluated consequences and, this matters, the engine will never resolve it. Choosing the restaurant is human work, injected as a resolution (you will do exactly that in Resolving Decides). When it resolves, it emits hold venue(dinner) = verde, and that is the assertion maya's gap is waiting for.

seek eta(dinner) by 19:00 means raj wants to know when maya arrives, by seven. No escalation clause: if it goes unmet, it simply stays open.

seek status(atlas.review) by thu else sync is raj's standing interest in the review he is owed, with the strongest escalation in the language: else sync authorizes the mesh to schedule live human time if the gap survives past Thursday.

bond maya { trust high } and raj's membrane and attention are the mirror image of maya's declarations: maya is family to raj, his decisions and venue facts flow to family exact, and he budgets four interruptions a day, with no quiet hours declared.

The settling story

Now keep the whole mesh in your head and watch what the pressure function will do with it. The story is narrated here as spec §8 tells it; in the next chapter we watch it happen.

t₀. Raj's seek eta(dinner) and maya's hold eta(dinner) form a gradient. Maya's membrane consults its rules: raj is family (she bonds him trust high), so the cast is exact. The pressure clears raj's family threshold, and the delta is absorbed silent. Raj's phone shows nothing. Raj's twin simply now knows 19:40. This is the sentence to sit with: the highest-volume outcome in Osmol is knowledge without an event.

t₁. Raj resolves decide venue = verde (a human judgment, injected from outside the mesh), which emits hold venue(dinner) = verde. Maya's seek venue gradient fires through raj's venue(*) -> family: exact rule. Because her gap carried else escalate, the answer takes ledger placement: it appears on her consequence-sorted board, with the deadline still distant and no interrupt spent.

t₂. Maya's owe review(atlas) auto-generated status supply meets raj's seek status(atlas.review). Her membrane's status(*) -> team: category rule casts it down: raj's twin now holds in-progress at class grain, silent. He knows the review is moving. He does not know, and is not entitled to know, anything finer.

t₃. And if Thursday arrives with the review gap still open? The else sync clause authorizes both membranes to book twelve minutes of live conversation, agenda pre-compiled from the surviving gap. Synchrony is the exception handler, not the ritual.

Total messages composed by humans: zero. Total interruptions: zero. Everyone knows everything they were entitled to know, the moment it mattered, and the mesh goes quiet, because silence is a fixpoint.

In the next chapter, we run this file through the reference interpreter and read the trace it prints, pressure arithmetic and all. The story above is what the numbers are about to say.

Reading the Trace

You have written the dinner mesh and injected raj's judgment. Now comes the payoff: the settlement trace, the most information-dense artifact the v0.1 interpreter produces. This chapter runs the canonical command and then walks the output line by line, until every number in it is something you could have computed yourself. If you are implementing Osmol in another language, this trace is your first golden file: your engine is correct when it prints the same story.

The canonical run

From the directory containing dinner.osmol:

python3 -m osmol dinner.osmol --resolve "raj:venue(dinner)=verde"

The complete output:

OSMOL v0.1 - reference interpreter
parsed dinner.osmol: 2 twins, 0 sends (no such construct exists)
initial gapcount: 3   (Theorem 1 bound: equilibrium in <= 3 flows)
  [human judgment] raj resolves venue(dinner) = verde
  human-lane  maya -> raj  (verbatim, provenance=human): "Saw a fox on the way home and thought of you."
t1  raj.venue(dinner) --exact--> maya   P=1.30 (R1.0*U1.3*T1.0*M1.0) > theta[family]=0.3   [ledger]
t2  maya.eta(dinner) --exact--> raj   P=1.30 (R1.0*U1.3*T1.0*M1.0) > theta[family]=0.3   [silent]
t3  maya.status(atlas.review) --category--> raj   P=0.65 (R1.0*U1.3*T1.0*M0.5) > theta[family]=0.3   [silent]

EQUILIBRIUM after 3 flows (Theorem 1 bound 3: respected)
messages composed by humans: 0 (the grammar has no verb for it)
interruptions: 0
ledger[maya]: venue(dinner) = verde
open gaps: 0 — silence is a fixpoint

Fifteen lines. Two people coordinated a dinner and a code review inside them, and neither of them wrote a word.

Line by line

The parse line. parsed dinner.osmol: 2 twins, 0 sends (no such construct exists) is not a joke. It is a claim the interpreter can back. The grammar contains no transmission construct, so the count of sends is zero by construction, in every program, forever. See What Cannot Be Written.

The header. initial gapcount: 3 counts every open seek in the mesh: maya seeks venue(dinner), raj seeks eta(dinner), and raj seeks status(atlas.review). The parenthesis states the quantitative bound of Theorem 1 before settling begins: because absorption is monotone (every flow closes exactly one gap and opens none), equilibrium must arrive in at most three flows. The engine asserts this bound at runtime; if any implementation ever exceeds it, the assertion trips and the implementation has confessed to betraying the semantics.

The human judgment. [human judgment] raj resolves venue(dinner) = verde records the resolution you injected with --resolve. The engine cannot make this choice; machines do not choose venues, in v0.1 or ever. It is a permanent feature of the runtime contract (see Resolving Decides). The resolution deletes raj's decide and emits hold venue(dinner) = verde, which is what gives the mesh something to equalize.

The human lane. Before any flow fires, the lane delivers:

  human-lane  maya -> raj  (verbatim, provenance=human): "Saw a fox on the way home and thought of you."

This is Axiom V made visible. The fox note is the one piece of free prose in the program, and it crosses first, untransformed, unsummarized, and provenance-labeled. No membrane rule touched it; none is allowed to (O-004).

The flow lines. Each firing flow prints its full anatomy:

t1  raj.venue(dinner) --exact--> maya   P=1.30 (R1.0*U1.3*T1.0*M1.0) > theta[family]=0.3   [ledger]

Read it as: at step t1, raj's holding venue(dinner) crossed to maya under the membrane cast exact, with pressure 1.30, clearing maya's threshold for the family sender class, and landing on the ledger. The arithmetic in parentheses is the pressure function of the spec, P = R × U × T × M − C, with the v0.1 constants:

• R = 1.0: relevance is exact fact-name matching in v0.1, so every match scores 1.0.
• U = 1.3: the gap carries a deadline (by 18:00), and any deadline sets urgency to 1.3, because wall-clock time is not simulated (a documented pragma).
• T = 1.0: the receiver bonds the sender trust high (high = 1.0, medium = 0.6, low = 0.3).
• M: the membrane cast weight: exact = 1.0, coarse = 0.7, category = 0.5, existence = 0.3, deny = 0. Watch t3: maya's membrane grants raj only category for status facts, so M drops to 0.5 and P falls to 0.65. That is still above threshold, so the flow fires, but raj's twin learns only the class-level fact.
• C = 0.0: attention cost, zero in v0.1 because interrupts are never spent (no wall clock).

The threshold on the right of the > is the receiver's, per Axiom III: maya bonds raj trust high, so raj is in maya's family class, whose default θ is 0.3 (team defaults to 0.4, others to 0.8). The sender did nothing to earn passage except be trusted by the receiver.

One subtlety: t1 and t2 both score 1.30. The dissertation fixes the tie-break as lexicographic by (sender, receiver, fact); the v0.1 interpreter uses iteration order instead, and here the two disagree: the lexicographic rule would fire maya's eta before raj's venue. A conforming successor must implement the lexicographic rule, see the pragmas chapter and the honesty note in the pressure chapter.

The placement tags. [ledger] and [silent] are the last stage of each flow. Maya's venue gap was declared else escalate, so its absorbed delta surfaces on her consequence-sorted board: ledger[maya]: venue(dinner) = verde. Everything else settles silently: raj's twin simply now knows maya's ETA and the review status, and no screen lit up to say so.

The footer. EQUILIBRIUM after 3 flows (Theorem 1 bound 3: respected) means the mesh used exactly its budget of demand, no more. Then the closing audit: zero messages, zero interruptions, one ledger entry, and open gaps: 0 — silence is a fixpoint, which is the third clause of Theorem 1 (zero_is_equilibrium) visible in the output. A mesh with no gaps admits no flow. The program is done not because anything halted it, but because there is nothing left to want.

Zero and zero

messages composed by humans: 0 and interruptions: 0 are not incidental statistics. They are the success metric, the one the Fifty-Year Letter calls perverse by 1971 standards: fewer human messages, warmer ones. Law IV reserves the human lane for what is irreducibly human, and the fox note is exactly that; everything else in this trace was logistics, and logistics equalized without spending a second of attention from either person.

Under the old paradigm, this same coordination costs a thread: "what time are you arriving?", "did you pick a place?", "how's the review going?". Three questions, so also three notifications and three context switches. Here the questions were gaps, the answers were holdings, and the mesh did the rest. Maya's phone showed one ledger line and one moment of warmth. Raj's phone showed the fox.

That is what a working Osmol implementation looks like from the outside: almost nothing. The quiet is not emptiness; it is the sound of the mesh settling. When your own implementation prints this trace byte for byte, you have carried the stone one habitat further.

Next: Resolving Decides covers the --resolve mechanism in depth, and the semantics chapters explain why this loop must always terminate.

Resolving Decides

The dinner mesh from the previous chapter contains one declaration the equilibrium engine will never touch on its own:

decide venue(dinner) among { verde, banh-mi-house } by 18:00

This chapter is about what happens when you run the mesh without answering that question, and about the one flag that exists for answering it.

Machines do not choose venues

Run the dinner mesh with no resolution:

$ python3 -m osmol dinner.osmol
OSMOL v0.1 - reference interpreter
parsed dinner.osmol: 2 twins, 0 sends (no such construct exists)
initial gapcount: 3   (Theorem 1 bound: equilibrium in <= 3 flows)
  human-lane  maya -> raj  (verbatim, provenance=human): "Saw a fox on the way home and thought of you."
t1  maya.eta(dinner) --exact--> raj   P=1.30 (R1.0*U1.3*T1.0*M1.0) > theta[family]=0.3   [silent]
t2  maya.status(atlas.review) --category--> raj   P=0.65 (R1.0*U1.3*T1.0*M0.5) > theta[family]=0.3   [silent]

EQUILIBRIUM after 2 flows (Theorem 1 bound 3: respected)
messages composed by humans: 0 (the grammar has no verb for it)
interruptions: 0
open gap [maya]: venue(dinner)
awaiting human judgment [raj]: venue(dinner) among ['verde', 'banh-mi-house']  (machines do not choose venues)

Everything that could settle, settled: raj's twin absorbed maya's ETA and the review status, two flows, both silent. But only two of the three gaps closed. Maya's seek venue(dinner) by 18:00 else escalate stays open, its escalation policy still armed, because the only possible supply for it is raj's decide, and the engine reached equilibrium around it. The final line is the interpreter refusing, in so many words:

awaiting human judgment [raj]: venue(dinner) among ['verde', 'banh-mi-house']  (machines do not choose venues)

This is not a stuck state. It is an equilibrium that happens to contain an open question addressed to a person.

The --resolve flag

A resolution is an injected human judgment. The syntax is twin:fact=value, and the flag is repeatable, one per pending decision:

$ python3 -m osmol dinner.osmol --resolve "raj:venue(dinner)=verde"

$ python3 -m osmol mesh.osmol --resolve "raj:venue(dinner)=verde" --resolve "maya:decision(atlas.budget)=approve"

Resolutions are applied before settling begins. The first thing settle() in osmol.py does is walk the --resolve list. For each one, it deletes the pending decide and emits the corresponding assertion: hold venue(dinner) = verde appears on raj's twin, and the trace records it as an input, not a flow:

  [human judgment] raj resolves venue(dinner) = verde

From that point the engine treats the new hold like any other supply. Maya's waiting seek venue(dinner) now has a matching holder; raj's membrane rule venue(*) -> family: exact grants it; the flow fires and lands on maya's ledger (her seek said else escalate). Run it and the mesh settles fully: three flows, then open gaps: 0 — silence is a fixpoint. The full resolved trace is walked line by line in Reading the Trace.

Notice the shape of this: the human did not compose a message announcing the venue. The human answered a question their own twin was holding open, and the mesh did the telling.

Guard rails

A resolution must name one of the declared options of the decision. The options are the contract. decide enumerates the acceptable answers at declaration time, and the interpreter enforces this:

$ python3 -m osmol dinner.osmol --resolve "raj:venue(dinner)=sushi-bar"
OSMOL v0.1 - reference interpreter
parsed dinner.osmol: 2 twins, 0 sends (no such construct exists)
osmol: resolution 'sushi-bar' not among options for venue(dinner)

A resolution naming a fact with no pending decide on that twin is simply ignored: there is no decision to resolve, so nothing happens. (Stricter behavior here is a reasonable thing for a future implementation to propose; see the RFC process.)

Why this is permanent

It would be a few lines of Python to make the engine pick the first option, or the highest-scoring one, or the one a language model likes. Those lines will never be written, in this or any implementation.

The engineering dissertation states it as a runtime-contract clause: human judgment is an input type, not a solver capability. decide blocks resolve only through an injected resolution, in every habitat (CLI, browser, edge, phone), always. The refusal of the interpreter to pick the restaurant is not a v0.1 limitation waiting for a smarter solver; it is a feature of the contract, exactly as load-bearing as the absence of send.

The reasoning runs straight back to the Seven Laws. Law IV reserves judgment, trust, and warmth for humans; the job of the mesh is to move logistics out of their way. A system that chooses on your behalf has not saved you a decision; it has taken one. So the boundary is drawn in the way this grammar prefers: not as a configuration option or a permission, but as an impossibility. The solver has no rule that touches a decide. Equilibrium is defined around open decisions, and the trace prints them as what they are: questions, waiting for the only kind of participant entitled to answer them.

For the full syntax and semantics of the construct (deadlines, option lists, and how a resolved decision becomes an assertion), see decide.

The Five Axioms

Every rule in the Osmol specification derives from five axioms. This is meant literally: when a construct seems strangely strict, when a piece of syntax you expect turns out not to exist, when an error message reads more like a principle than a diagnostic, one of these five is the reason. An implementer who knows the axioms well can usually predict the rest of the language before reading it.

The axiom statements below are quoted verbatim from spec §1. The commentary after each is what the axiom costs you as an implementer: the machinery it obligates you to build, and the machinery it forbids you to build.

Axiom I. There is no send.

There is no send. No construct exists that transmits content to a party. Communication occurs only as the mesh's resolution of pressure between declared states. The sender, as a grammatical role, does not exist.

For implementers: your grammar must have no transmission production, and your toolchain must enforce that absence actively. The tombstone words (send, notify, broadcast, blast, cc, bcc, forward, reply) are reserved solely to produce O-000; the old world's verbs die loudly, not quietly. Everything that looks like delivery in a running mesh is in fact the solver resolving pressure between a hold and a seek. There is no code path in which one twin pushes content at another.

Axiom II. Programs are claims, not commands.

Programs are claims, not commands. Every statement is a declarative speech act: an assertion, a gap, a commitment, a decision, an expression, or a permission. There are no loops, no sequencing, no control flow. Order of declarations never matters.

For implementers: you are building a constraint settler, not an instruction executor. There is no program counter, no statement ordering to preserve, no evaluation order to document. Order-irrelevance is strong enough that a formatter is free to sort declarations canonically. The dissertation's osmol fmt does exactly that, because reordering cannot change meaning. If your implementation's output ever depends on the textual order of declarations (beyond the spec's deterministic tie-break on pressure, which is by (sender, receiver, fact), not by line number), you have a bug.

Axiom III. The receiver's grammar governs.

The receiver's grammar governs. Thresholds, budgets, and quiet hours are properties of the receiving twin, declared in the receiving twin's source, and no construct in any other twin's source can reference, lower, or spend them.

For implementers: attention and membrane blocks attach syntactically to the twin that owns them, and the grammar provides no way to name a foreign twin's blocks at all. This is deliberately enforced before type checking, by the shape of the syntax tree. See O-006 and O-001 for the two diagnostics that guard the property at the AST level, where tools might construct what the parser cannot.

Axiom IV. Precision only flows downhill.

Precision only flows downhill. Every value carries a granularity, and the type system admits transforms only downward along the lattice exact ⊒ coarse(g) ⊒ category ⊒ existence. Coarsening is a cast; refinement is a type error. Precision cannot be manufactured, only surrendered.

For implementers: every value in your representation carries a granularity coordinate, and every membrane transform is a cast checked against the lattice. There is no syntax for an upward cast (the grammar simply has no word for it), and an AST-level attempt is O-002. The open formal counterpart is Theorem 4 (granularity monotonicity along composed flow paths); see The Open Ledger.

Axiom V. The human lane is verbatim.

The human lane is verbatim. Expressive content crosses the mesh untransformed, unsummarized, and provenance-labeled. No transform, membrane rule, or attention rule may compress it, and no autonomous process may author it.

For implementers: express content is exempt from every transform in your pipeline. A membrane or attention rule whose selector matches an expression is O-004; an expression authored by an autonomous process is O-005. Quiet hours may queue an expression; nothing may summarize or silence one. Provenance (human by default, assisted permitted, autonomous unrepresentable) travels with the content.

A table of consequences

Each axiom appears three times in the language: as a principle, as a grammar feature, and as a diagnostic. Reading across a row is the fastest way to see that the errors are the ethics.

Axiom II is the only row without a diagnostic, and that too is a consequence: a property that holds because the grammar has no way to violate it needs no error message. The full catalog of impossible sentences lives in What Cannot Be Written.

The Speech-Act Type System

Where conventional languages type data (int, string), Osmol types acts. Every top-level statement inhabits exactly one of five kinds, and the kind determines how the equilibrium engine treats it. This section is spec §3; treat it as the map of the whole constructs reference.

Assertion (hold): a claim that the twin possesses a value, with optional uncertainty, confidence, and decay. Assertions are the mesh's supply side.

Gap (seek): a first-class record of absence, meaning the twin lacks a value and registers standing interest. Gaps are the demand side, and the only thing that can attract flow. A gap may carry a deadline and an escalation policy.

Commitment (owe): a promise from this twin to a party, with a due instant. Commitments generate structural gaps automatically: an unmet owe implies the counterparty's seek for its status.

Decision (decide): an open choice among enumerated options with a deadline. Decisions are gap generators (one gap per option's unevaluated consequences) and emit an assertion upon resolution.

Expression (express): human-lane verbatim content directed to a party, carrying mandatory authorship provenance (human by default; assisted permitted; autonomous unrepresentable, see O-005).

Two auxiliary families complete the system. Permissions: membrane, whose rules are typed as granularity casts guarded by conditions. Postures: attention, bond, role, and stake, which parameterize the pressure function rather than the state.

Values are typed as quantity, instant, place, enum, or entity, each carrying a granularity coordinate. The full type of an assertion is therefore a triple: (value type, granularity, temporal validity), for example:

place @ exact, decays 20:00

read as: a place-typed value, at exact granularity, valid until 20:00. All three coordinates matter to the engine. The value type drives relevance matching between holds and seeks; the granularity coordinate is what membrane casts operate on (granularity); and temporal validity feeds the urgency term of the pressure function (pressure).

If you carry only one thing from this page into an implementation, let it be this: the five kinds are not statement categories for documentation purposes. They are the type system. Each kind has a distinct role in the engine (supply, demand, structural demand, demand-generation-plus-eventual-supply, and the protected verbatim lane), and every downstream rule in the language (what flows, what casts, what may never be touched) dispatches on that kind first.

Lexical Structure

This page restructures §2 of the specification as a reference for implementers. Osmol's lexical layer is small on purpose, but it is opinionated: the token set itself encodes the language's physics of knowledge, and one class of tokens exists only to die loudly.

Source form

Osmol source is UTF-8. Comments run from -- to end of line:

hold eta(dinner) = 19:40 ±5m, decays 20:00   -- uncertainty and decay, inline

Identifiers are lowercase kebab-case or dotted paths:

banh-mi-house
atlas.budget
status(atlas.review)

There is no uppercase convention to learn because there are no types to name, no classes to export, and no constants to shout. A twin's vocabulary is facts about a life, and facts are lowercase.

Literal forms

The literal forms are chosen so that time, uncertainty, and decay (the physics of knowledge) are first-class tokens rather than library calls. A value in Osmol is a datum with a shelf life, an error bar, and a resolution.

A holding like hold eta(dinner) = 19:40 ±5m @0.9, decays 20:00 is therefore expressible without a single library import: the instant, its uncertainty, its confidence, and its expiry are all lexical.

Strings

Strings are double-quoted and legal only inside express. This is Axiom V doing lexical work: prose is a controlled substance. Everywhere else in the language, values must be typed literals a machine can reason about: an eta is an instant, not a sentence about an instant. Free text exists in exactly one construct, the human lane, where it crosses the mesh verbatim and provenance-stamped. A string outside express is not a style violation; it does not tokenize.

Reserved words

The reserved words, exactly as spec §2 lists them:

twin, hold, seek, owe, decide, among, express, to, membrane, attention,
bond, trust, assume, yield, role, stake, on, toward, by, else, when,
decays, until, every, interrupts, quiet, threshold, escalate, sync,
drop, exact, coarse, category, existence, deny, family, team, others, all

Thirty-nine words. This is the entire keyword surface of the language, and none of them is a verb of transmission.

Tombstone words

A second reserved list exists for one purpose only, producing a compile error:

send, notify, broadcast, blast, cc, bcc, forward, reply

These eight words are reserved solely to fire error[O-000]: there is no send. They have no production in the grammar, no semantics, and no future. They exist so that the old world's verbs die loudly rather than quietly. A newcomer who types send gets the whole philosophy of the language in one diagnostic instead of a confusing unexpected identifier.

Implementers: the tombstone check should be the fastest error your toolchain can produce. The engineering dissertation places it at the lexer, before parsing exists.

Implementation note: how v0.1 tokenizes

The reference interpreter (osmol.py, normative for v0.1 behavior) does not run a general tokenizer. It works line by line: each line is stripped of comments, then matched against a table of regular expressions (the RX table), one pattern per declaration form. A line that matches no pattern is an unrecognized declaration, and that is a hard error. There is no "unknown statement, skipping" in this language.

Two ordering rules in osmol.py are worth carrying into any implementation:

1. Tombstones are checked before anything else. Every line passes tombstone_check before any declaration pattern is tried, so send dies with O-000 even inside an otherwise unparseable line.
2. Strings are stripped first. The tombstone check removes double-quoted spans before scanning for tombstone words, because strings are payload: express to raj: "I will reply tomorrow" is legal. The human lane may say anything; only the grammar is forbidden the old verbs.

The line-oriented approach is a documented v0.1 pragma, not the language's final word. The Rust core specifies a handwritten lexer with proper spans (dissertation, Chapter 2). But the two rules above are semantics, not implementation detail: keep them.

Related

• The Formal Grammar: the EBNF these tokens feed
• What Cannot Be Written: the load-bearing absences
• O-000, Tombstone Verb: the diagnostic the tombstone list exists for
• Granularity: the lattice behind coarse(...) grains

hold, Assertions

An assertion is a claim that the twin possesses a value. Assertions are the mesh's supply side: they are what flows when a matching gap pulls, and they never move for any other reason. A hold with no seeker is inert: declared, membrane-guarded, and perfectly silent.

Syntax

From the grammar in spec §5:

hold        = "hold" fact "=" value [ "±" quantity ] [ "@" number ]
              [ [","] temporal ] ;

temporal    = "decays" ( instant | reltime )
            | "until" instant
            | "every" period ;

Semantics

A hold declares that this twin holds a value for a fact, with three optional refinements:

• Uncertainty (±): an honest error bar on the value itself. 19:40 ±5m means "around 19:40, trust me to five minutes." The uncertainty is part of the claim, not a hedge added afterward.
• Confidence (@): how sure the twin is that the claim is true at all, from @0.0 to @1.0, defaulting to @1.0.
• Temporal validity: when the claim stops being a claim. decays gives an expiry (absolute or relative), until a hard end, every a refresh period. Knowledge in Osmol is perishable by declaration, so nobody has to remember to retract an ETA after dinner.

The full type of an assertion is therefore a triple: (value type, granularity, temporal validity), for example place @ exact, decays 20:00. Value types are quantity, instant, place, enum, or entity, and every one of them carries a granularity coordinate on the lattice. What a given receiver actually absorbs is this value after the owning twin's membrane casts it downward; the assertion itself always stays at its declared grain.

Assertions participate in settling exactly one way: when some other twin's seek matches the fact, the pressure function evaluates the pair, the membrane supplies the cast, and if pressure clears the receiver's threshold, a delta flows and the gap closes. Order of declaration never matters; a hold is a fact about the world, not a step in a procedure.

Examples

The three from spec §4.2:

hold eta(dinner) = 19:40 ±5m, decays 20:00
hold location(office) = grid(52.52, 13.40), decays +2h
hold status(atlas.review) = in-progress @0.9

An instant with uncertainty and decay; a place with a relative decay; an enum with explicit confidence. Three claims, and each one is honest in its own way.

In the v0.1 interpreter

osmol.py keeps assertions in twin.holds, a map from fact string to uninterpreted value string: "19:40 ±5m" is stored and flowed as text, not parsed into an instant plus an error bar. decays and until clauses are parsed by the hold regex but wall-clock time is not simulated, so nothing actually expires during a settle. This is a documented pragma, not an accident (see v0.1 pragmas).

Two constructs auto-emit holds, so your twin can hold more than you wrote:

• owe emits structural supply at parse time: owe review(atlas) to raj by fri also creates hold status(atlas.review) = in-progress on the ower, because an unmet commitment implies the counterparty's interest in its status.
• A resolved decide emits its outcome: injecting raj:venue(dinner)=verde deletes the pending decision and creates hold venue(dinner) = verde.

Both are how the dinner mesh's second and third flows come to exist without maya or raj writing a single extra line.

Related

• seek, the demand side; the only thing a hold can flow toward.
• membrane, who may see this assertion, and at what grain.
• O-002, the error you get for trying to sharpen a held value on its way out.
• The granularity lattice, where the grain coordinate lives.

seek, Gaps

A seek declares a gap: a first-class record of absence. The twin lacks a value and registers standing interest in obtaining it. Where hold is the mesh's supply side, seek is its demand side, and demand is privileged. A gap is the only thing that can attract flow. No holding moves anywhere, at any pressure, unless a matching gap exists on the receiving side: no gap, no gradient.

Syntax

From the spec §5 grammar:

seek        = "seek" fact [ "by" instant ] [ "else" escalation ] ;
escalation  = "escalate" | "sync" | "drop" ;

Examples from spec §4.3:

seek location(dinner) by 19:00 else escalate
seek decision(atlas.budget) by fri else sync
seek weather(berlin, sat)                  -- standing gap, no deadline

A seek names a fact the twin is missing, optionally a deadline (by), and optionally what should happen if the deadline arrives with the gap still open.

Semantics

A gap does three things. It registers demand, so the pressure function has something to evaluate: the gradient engine only computes P(A→B, k, g) over pairs where A holds k and B seeks a matching g. It carries urgency: the gap's deadline feeds the U term, so pressure rises as the deadline nears. And it defines its own closure: when a flow fires and B absorbs the understanding-delta, the gap is popped from B's state and the pressure term collapses to zero. Absorption is monotone (a delta closes exactly one gap and opens none), and this is the load-bearing fact behind Theorem 1.

Escalation policies

The spec §4.3 defines the three else policies:

else escalate promotes the gap's urgency term as the deadline nears; else sync authorizes the mesh to schedule live human time if the gap survives past deadline; else drop lets it lapse.

else sync deserves a short remark. It is the language's hook into the protocol's escalation to synchrony: when a gap outlives its deadline, the membranes on both sides are authorized to book a short live conversation, with the agenda pre-compiled from the surviving gaps; spec §8's trace puts it at twelve minutes. Synchronous human interaction becomes the system's exception handler rather than its default ritual. A meeting in Osmol is what happens when equalization fails, and it arrives with its agenda already written.

else drop is the humble one: some curiosity has a shelf life, and a gap that lapses quietly costs no one anything.

Structural gaps

Not every gap is written with the word seek. Per spec §3, commitments and decisions imply gaps structurally: an unmet owe implies the counterparty's seek for its status, and an open decide generates gaps for each option's unevaluated consequences. In the dinner mesh, maya's owe review(atlas) to raj is what gives raj's seek status(atlas.review) something to drink from. The commitment auto-generates the supply that the structural demand attracts.

The three origins

The Osmosis Protocol spec (§2) names three ways gaps arise:

• Explicit: the participant asks a question, recorded as a gap rather than transmitted as a message. This is the seek keyword.
• Structural: open decisions and commitments imply missing inputs, as above.
• Predictive: an on-device model infers that a value will be needed before a time T and pre-registers the gap, conservatively weighted.

The first two exist in the language today. Predictive gaps are protocol-future: the provisional spec describes them, but Osmol v0.1 has no syntax or semantics for them yet. When they arrive, they will arrive through the RFC process.

What you cannot write

A seek can only name a fact its own twin lacks. The grammar has no production that lets one twin declare a gap on another twin's behalf. That is diagnostic O-001: cannot want on maya's behalf. Gaps belong to their owners. And constructing pressure toward a twin with no matching gap is O-003: no gap, no gradient. Stake reputation or remain silent, with stake as the sole, priced exception.

v0.1 interpreter notes

The reference interpreter implements gaps with these documented pragmas:

• Deadlines set U = 1.3. Wall-clock time is not simulated, so any by clause raises the urgency term to 1.3 uniformly; there is no gradual promotion as the deadline nears.
• escalate places on the ledger. A gap tagged else escalate has its absorbed delta placed [ledger]; all other absorbed deltas are [silent].
• sync prints its promise. A sync-tagged gap still open at equilibrium prints -> sync will be scheduled (else sync); actual scheduling needs a wall clock and a second device, neither of which v0.1 has.
• Absorption pops the gap. One flow, one gap closed, monotonically. The engine asserts Theorem 1's bound (flows ≤ initial gapcount) at runtime.

Related

hold · owe · decide · Pressure · O-001 · O-003

owe, Commitments

Syntax

owe = "owe" fact "to" party [ "by" instant ] ;

From spec §4.4:

owe review(atlas) to raj by fri
owe photos(hiking-trip) to family by sun

Semantics

An owe is a commitment: a promise from this twin to a party, with a due instant. It is one of the five speech-act kinds (spec §3), and its defining property is that commitments generate structural gaps automatically: an unmet owe implies the counterparty's seek for its status.

Read that twice, because it is the construct doing the most quiet work in the language. When you promise something, the mesh does not wait for the other side to ask "how's it going?" The promise itself creates the demand-and-supply structure that keeps the counterparty informed. Nobody composes a status report; status is a consequence of having promised.

Case study: the dinner mesh, t₂

In the canonical maya/raj program (spec §8), maya declares:

owe review(atlas) to raj by fri

and raj, independently, declares:

seek status(atlas.review) by thu else sync

The spec's trace describes what happens at t₂: maya's owe review(atlas) auto-generates status pressure against raj's seek status; her membrane rule status(*) -> team: category casts it down, and raj's twin absorbs in-progress, placed silent. Raj knows the review is moving without either human writing a word. And if Thursday arrives with the review gap still open, raj's else sync clause authorizes both membranes to book live conversation, agenda pre-compiled from the surviving gap. The commitment escalates itself.

In v0.1 (normative pragma)

The reference interpreter implements the structural-gap rule from the supply side, and this pragma is normative for v0.1; any implementation must honor it or consciously supersede it through an RFC:

owe X(args) auto-emits hold status(args.X) = in-progress on the ower.

Concretely, in osmol.py's parser: owe review(atlas) to raj by fri records the commitment and immediately emits hold status(atlas.review) = in-progress on maya's twin (the fact's argument and name swap into a dotted path; an argument-less owe done() would emit hold status(done())). The setdefault matters: if the ower has already declared a more precise status by hand, for example hold status(atlas.review) = in-progress @0.9, the auto-emitted default does not overwrite it.

This is how commitment-status supply exists without anyone composing a status report. The ower's side of the structural gap is materialized eagerly as a holding; the counterparty's implied seek is left to be declared explicitly in v0.1 (raj writes his own seek status(atlas.review)), which is the pragma's honest simplification of the spec's fuller "implies the counterparty's seek" semantics.

The philosophy: Law III

The owe construct is Law III of the Fifty-Year Letter, Compiled State, enforced by grammar. Conversation must compile; the build artifact is a living, queryable state of commitments and their owners; and the hard rule follows: if it is not in the state, it was not decided. An obligation smeared across a message thread is archaeology. An owe is a record: it has an owner, a counterparty, a due instant, and a machine-readable status from the moment it exists. The ledger view of your mesh (see placement, in the equilibrium model) is exactly this: commitments you owe, commitments owed to you, sorted by consequence rather than arrival.

Related

• seek, the demand side an unmet owe implies.
• decide, the other construct that generates gaps from its own structure.
• Equilibrium and placement, how commitments surface on the ledger.
• The v0.1 pragmas, the complete normative pragma list.

decide, Decisions

A decide declares an open choice: this twin must pick one of an enumerated set of options, usually by a deadline. It is the fourth of the five speech-act kinds (The Five Axioms), and it is also the one construct in the language whose completion the engine is forbidden to perform.

Syntax

From spec §5:

decide      = "decide" fact "among" "{" value { "," value } "}"
              [ "by" instant ] ;

The example from spec §4.5, verbatim:

decide venue(dinner) among { verde, banh-mi-house } by 18:00

Semantics

Spec §3 gives decide a dual role in the engine:

• Gap generator. An open decision implies missing inputs: it generates gaps for each option's unevaluated consequences. Demand radiates from an unresolved choice.
• Assertion emitter. Upon resolution, the decision emits an assertion: the chosen value becomes a hold, and from that moment it is ordinary supply that can flow to any counterparty whose seek matches and whose membrane passage is granted.

Between declaration and resolution, the decide simply stands open. Nothing in the mesh can force it closed.

Resolution: injected human judgment

Who closes it, then? A human, always, and only a human. In v0.1 a resolution arrives on the command line:

python3 -m osmol dinner.osmol --resolve "raj:venue(dinner)=verde"

The resolved decide becomes, in effect, hold venue(dinner) = verde on raj. That new hold then satisfies any counterparty seeks: in the dinner mesh this is exactly flow t₁, where maya's seek venue(dinner) by 18:00 else escalate finally has supply to draw on, and the venue flows to her ledger. The walkthrough is in Resolving Decides.

This is not a v0.1 shortcut that waits for a smarter engine. It is the permanent contract of the runtime, in every habitat, always: the engine cannot choose. The dissertation states it as design law, human judgment is an input type and not a solver capability, and the reference interpreter states the same in a comment at the exact point where resolutions enter the engine:

human judgments arrive as declarations, never as choices the machine makes on a person's behalf

Any future implementation that "helpfully" resolves a decide, even an obviously one-sided one, is nonconforming. A mesh that picks your restaurant is a mesh that will eventually pick your answer.

v0.1 interpreter notes

The reference interpreter's handling, normative for v0.1:

• Parsing. The options list is parsed into a per-twin decides dict: fact -> {"among": [...], "by": ...}.
• Validation. A --resolve value is checked against the declared options set; a value not among the options is an error (resolution 'X' not among options for fact). You cannot inject a choice the program never enumerated.
• Resolution. A valid resolution deletes the decide, installs the chosen value as a hold, and prints a [human judgment] line in the trace.
• Unresolved decides do not block. All other flows settle normally around an open decision; at equilibrium the interpreter reports each one:

awaiting human judgment [raj]: venue(dinner) among ['verde', 'banh-mi-house']  (machines do not choose venues)

Note that "equilibrium" and "everything resolved" are different states. A mesh with an open decide can be perfectly settled (no pressure clears any threshold) while it still waits on a person. The final silence is a fixpoint line prints only when open gaps and pending decides are both zero.

• Structural gaps are simplified. Spec §3's per-option consequence gaps are not materialized as first-class gaps in v0.1; the decide's demand shows up through counterparty seeks (like maya's seek venue) rather than through auto-generated internal gaps. An implementation targeting the full spec should generate them.

Related

• Resolving Decides, the tutorial walkthrough of --resolve on the dinner mesh
• owe, the other structural-gap generator (commitments)
• seek, the gaps a resolved decision ultimately satisfies

express, The Human Lane

Syntax

express = "express" "to" party ":" string ;

Semantics

express is the only construct in Osmol that admits free prose. Everything else in the language is typed literals a machine can reason about; here, and only here, a double-quoted string is legal (Lexical Structure).

The spec's example, §4.6:

express to mom: "Saw a fox on the way home and thought of you."

An expression crosses the mesh verbatim, provenance-stamped, and immune to every transform and every attention rule. No membrane rule may coarsen it, no summarizer may compress it, and no classifier may silence it. It may be queued by the receiver's quiet hours, but never summarized or silenced. This is Axiom V: the human lane is verbatim. Two diagnostics guard it structurally: a membrane or attention rule whose selector matches an express is error[O-004], and the transform simply has no grammar to apply.

Every expression carries a mandatory authorship provenance class:

• human: the default. A person composed these words.
• assisted: a machine helped; a person directed and owns it.
• autonomous: unrepresentable. An express authored by an autonomous process is error[O-005]: machines may not counterfeit the human lane. This is not a policy setting; the provenance class has no legal spelling.

Why it exists

A fair objection to a mesh that resolves logistics without human messages is what the Fifty-Year Letter's objections chapter calls the death of texture: if agents write to agents, do humans stop hearing each other? Osmol's answer is architectural, not aspirational. Laws IV and V of the letter split the lanes (machines exchange state, humans exchange meaning), and the system must protect unstructured, inefficient, warm communication on purpose. Efficiency is for machines; presence is for people.

So the human lane is deliberately inefficient by design (Osmosis protocol spec, §9): no summarization, no batching, full fidelity. The stated design objective is that traffic in every other lane falls while traffic in this lane rises in warmth per unit. The fox line above is the canonical specimen: it carries no fact, closes no gap, and answers no deadline. It exists because its exact wording is the point, and the grammar guarantees that the wording survives.

The provenance requirement answers the darker failure mode the letter names: the automation of intimacy. A birthday message ghost-written by a model must not be able to masquerade as a human act. In Osmol, it grammatically cannot.

In v0.1

The reference interpreter delivers expressions first in settle(), before any flow is evaluated: the human lane outranks the pressure engine in the event order itself. Each delivery prints verbatim with its provenance:

  human-lane  maya -> raj  (verbatim, provenance=human): "Saw a fox on the way home and thought of you."

You can see this live in The Dinner Mesh: dinner.osmol contains

express to raj: "Saw a fox on the way home and thought of you."

and its line is the first event of every settlement trace. Note the v0.1 pragmas: quiet hours are stored but not enforced (no wall clock is simulated), and provenance is always human because the interpreter has no autonomous authors to refuse.

The future: authorship as a cryptographic claim

In the full protocol (engineering dissertation, Chapter 5), the provenance label stops being metadata. Every delta is signed over payload, provenance chain, authorship class, and nonce, with keys held in device secure hardware. So "a human wrote this" becomes a cryptographic claim, and to forge it means to forge a signature. O-005 is the compile-time face of that guarantee; the signature is its runtime body.

Related

• O-004, Transformed Expression, the membrane may not touch this lane
• O-005, Counterfeit Humanity, machines may not author in it
• attention, quiet may queue expressions; nothing may silence them
• Lexical Structure, why strings live only here

membrane, Permissions as Casts

Most systems bolt permissions on as an afterthought: an ACL consulted at the door. Osmol types them. A membrane rule is a granularity cast, a typed statement of how much precision a given audience may receive, and the whole family of upward casts simply does not exist in the grammar. Privacy in Osmol is not a filter that fights at runtime; it is a property of which sentences can be written.

Syntax

From the grammar in spec §5:

membrane    = "membrane" "{" { flowrule } "}" ;
flowrule    = selector "->" party [ "when" condition ] ":" transform ;

selector    = fact | ident | "*" ;
party       = ident | "@role(" rolename ")"
            | "family" | "team" | "others" | "all" ;
transform   = "exact" | "coarse(" grain ")" | "category"
            | "existence" | "deny" ;

Each rule reads: facts matching this selector, flowing to this party, (optionally) when this condition holds, cross at this grain.

Semantics

The six-rule example from spec §4.7:

membrane {
  eta(*)        -> family:                exact
  eta(*)        -> others:                coarse(30m)
  location(*)   -> family when moving:    exact
  location(*)   -> others:                coarse(city)
  status(atlas.*) -> @role(lead, atlas):  exact
  finances(*)   -> all:                   deny
}

Transforms are downward casts. The five transforms are the four rungs of the granularity lattice (exact, coarse(g), category, existence) plus deny, which is the zero of the whole system. There is no syntax for an upward cast: you cannot write a rule that turns coarse(city) into exact, because the grammar's transform vocabulary has no word for refinement. Axiom IV, precision only flows downhill, is enforced by the parser's dictionary before any checker runs. Where a program tries to grant a grain finer than the holding actually has, the semantic checker answers with O-002.

Membranes belong to the twin they are inside. A membrane block governs the outbound flow of its own twin's holdings, and nothing else. The grammar cannot express "raj's membrane" from inside maya's twin; attempting to reference another twin's membrane or attention is O-006, and Axiom III is the reason: the receiver's grammar governs, and the sender's membrane governs the sender.

Selectors are fact patterns with * wildcards and dotted paths. eta(*) matches any eta fact; status(atlas.*) matches status(atlas.review) and everything else under the atlas project; a bare * matches all facts. Specific and general rules coexist; order decides between them (below).

Parties name the audience: a specific twin by name (raj), a semantic role (@role(lead, atlas)) resolved at flow time rather than bound to an endpoint, or one of the four audience classes family, team, others, all.

Conditions (when moving) gate a rule on the twin's own state, so precision can depend on context: exact location for family, but only while in transit.

The audit trail (future). The Osmosis protocol spec (§4) requires that every membrane decision be logged in an append-only record visible to the membrane's owner, and that the membrane be portable: its policy set and logs export in a standard format and rehost on any conforming mesh without loss. That portability is one of the two constitutional clauses of Osmol governance. No wire transport exists yet, so no implementation writes this log today, but any future one must.

Cast weights

Inside the pressure function P = R × U × T × M − C, the membrane's verdict becomes the factor M:

deny annihilates pressure entirely, and this is exactly the shape Theorem 2 (non-interference) needs, once it is proven: M = 0 means no delta derived from this twin's state can reach that party at all.

In the v0.1 interpreter

osmol.py implements membranes in membrane_cast, with four documented behaviors to honor or consciously supersede (see v0.1 pragmas):

• Rules match in declaration order, and the first match wins. Put specific rules above general ones; a leading eta(*) -> all: deny shadows everything after it for eta facts.
• No matching rule means no flow. membrane_cast returns None, and the engine treats that exactly like deny: default-deny is the resting state of every membrane. A twin with an empty membrane block shares nothing.
• The circles pragma. v0.1 has no social graph, so audience classes are derived from bonds: family and team match any party the sender bonds trust high; others matches everyone else; all matches everyone. This is why the dinner mesh's maya must bond raj { trust high } for her eta(*) -> family: exact rule to reach him.
• when conditions are parsed but not evaluated. The condition is captured into the rule tuple and then ignored: a when moving clause in v0.1 behaves as if always true. This is an honest gap between grammar and engine, and a good first RFC-shaped contribution.

Related

• The granularity lattice, what the casts are casts on.
• O-002, granularity inversion: precision cannot be manufactured, only surrendered.
• O-004, no membrane rule may match an express; the human lane is verbatim.
• O-006, foreign sovereignty: membranes and thresholds belong to their owners.

attention, The Sovereign Budget

The attention block is where a twin declares what its owner's mind costs. Interrupt budgets, quiet hours, and per-class thresholds all live here, and they live only here, inside the twin they govern. This is Axiom III in construct form: the receiver's grammar governs.

Syntax

From the spec §5 grammar:

attention   = "attention" "{" { budget } "}" ;
budget      = "interrupts" nat "/" period
            | "quiet" timerange
            | "threshold" party number ;

The spec §4.8 example:

attention {
  interrupts 3/day
  quiet 22:00-07:00
  threshold others 0.8
  threshold family 0.3
}

interrupts n/period caps how many times per period anything may render now. quiet a-b declares a time range in which even budgeted interrupts wait. threshold party x sets θ, the pressure bar a flow must clear, per sender class.

Semantics

The thresholds declared here are the θ in the flow condition: a flow from A to B fires iff P > θ_B(A), where the subscript order is the whole design. θ belongs to B, is declared in B's source, and is indexed by B's classification of A. Nothing A writes can lower it, spend it, or see it.

The spec is emphatic that this is enforced below the type system:

Budgets and thresholds are legal only inside the twin they govern. Referencing another twin's attention block is not a permission error at runtime; it is a parse-impossible construction (Axiom III).

There is no syntax tree in which twin maya contains a rule about raj's thresholds. An attempt to construct one at the AST level (by a tool, bypassing the parser) is diagnostic O-006: thresholds belong to receivers. This is the entire point.

Why a budget

The philosophy comes straight from the Fifty-Year Letter. Law I, Receiver Sovereignty: attention belongs to the person receiving, not the person sending; nothing reaches a human eye by default. And the attention-budget component of the successor architecture: interruptions are metered like money. Senders spend standing to claim them, and chronic overdrafters find the price of your attention rising. Herbert Simon diagnosed the disease already in 1971, the year email was born: a wealth of information creates a poverty of attention. The attention block is that diagnosis turned into grammar. For the first time the cost of a demand on your mind is written down, and it is written down by you.

The protocol behind it

The Osmosis Protocol spec (§6) describes the full placement mechanics this block parameterizes: every absorbed delta is classified silent, ledger, or interruption; interruptions debit the sender's standing against the receiver's budget, denominated per link and per period; chronic overdraft raises the effective θ for that sender; and an interruption-class delta must carry a declared consequence-if-ignored field, verified for plausibility. Most of that machinery is protocol-future; the language gives it a home today, and the mesh grows into it.

v0.1 interpreter notes

The reference interpreter honors this block with documented pragmas:

• Default thresholds. If a class has no explicit threshold, the defaults are family 0.3, team 0.4, others 0.8 (DEFAULT_THETA in osmol.py). Low bars for the trusted, a high bar for strangers.
• Class derives from the receiver's own bonds. For a given sender, the receiver's class is computed by theta_for from the receiver's bond declarations: if the receiver bonds the sender trust high, the sender is family; otherwise others. Note that v0.1's receiver-side classifier is binary: team exists in the default table and may be set explicitly, but the engine never assigns a sender to it. (On the sender side, team and family audiences both match trust-high bonds; see the circles pragma.)
• quiet is stored, not enforced. Wall-clock time is not simulated, so quiet hours are parsed and kept but never consulted.
• interrupts is modeled but unused. Interrupt placement requires a passed escalate deadline, which needs a wall clock; in v0.1, no flow ever places as interrupt, so budgets are never debited and every trace honestly reports interruptions: 0.

The full guarantee, that interrupt placements never exceed the declared budget for any behavior of any other twin, is Theorem 3 (Attention soundness), which is open. The grammar shape already does most of the work; the proof will make it an invariant rather than a courtesy.

Related

bond · membrane · Pressure · Equilibrium · O-006 · Open theorems

bond, Trust

Syntax

bond    = "bond" party "{" "trust" level "}" ;
level   = "low" | "medium" | "high" | number ;

From spec §4.9:

bond raj { trust high }

The grammar admits a numeric trust level; v0.1 parses the word levels only (low, medium, high). Numeric levels await a future edition.

Semantics

A bond declares this twin's trust toward a party. It is a posture, not a state: like attention, role, and stake, it parameterizes the pressure function rather than adding facts to the mesh. Specifically, it feeds T in the pressure product:

P(A→B, k, g) = R(k, g) × U(g, t) × T(A, B) × M(A→B, k) − C(B, t)

Trust is the term that makes the same fact, under the same membrane, flow easily between friends and hardly at all between strangers.

In v0.1: which bond, whose bond

The reference interpreter is precise about direction, and this precision matters. A bond does double duty, once on each side of a flow, and in both uses it is read from a specific twin's declarations:

On the receiving side, T is the receiver's bond toward the sender. In osmol.py's pressure(), the trust term is receiver.bonds.get(sender), defaulting to medium when no bond is declared. The weights are:

Your trust in someone amplifies what can reach you from them. Nothing the sender declares can raise it: writing bond ceo { trust high } in your own twin says you trust the CEO; it does not make the CEO trust you.

Also on the receiving side, bonds pick the threshold class. theta_for() classifies the sender as family if the receiver bonds them trust high, and others otherwise; the flow must then clear the receiver's declared threshold for that class (defaults: family 0.3, others 0.8; a team class exists in the defaults table but v0.1's classifier only produces family or others).

On the sending side, bonds define the membrane's circles. This is the circles pragma from the interpreter header: when a sender's membrane rule addresses the audience family or team, it matches any party the sender bonds with trust high; others matches the rest (audience_match() in osmol.py). So the same declaration that opens your threshold to a person also places them inside your intimate membrane audiences.

The practical consequence, in the dinner mesh

In dinner.osmol, maya declares bond raj { trust high } and raj declares bond maya { trust high }. Because the bond is mutual, each is "family" to the other twice over:

• When maya's eta(dinner) flows to raj, maya's membrane rule eta(*) -> family: exact matches raj (sender-side circle: maya bonds raj high), so raj gets the exact value rather than coarse(30m). On raj's side, T = 1.0 (raj bonds maya high) and the threshold class is family (0.3). The trace line shows all of it: P=1.30 (R1.0*U1.3*T1.0*M1.0) > theta[family]=0.3.
• Symmetrically, raj's venue(*) -> family: exact matches maya, and maya's threshold for raj is the family 0.3.

Delete one of the two bonds and the mesh degrades in a directionally honest way. If raj dropped his bond maya, every consequence would land in raj's own declarations. Incoming: maya's ETA would face T = 0.6 and raj's others threshold of 0.8, so P = 1.0 × 1.3 × 0.6 × 1.0 = 0.78, short of the bar, and the flow would not fire. Outgoing: raj's venue(*) -> family: exact rule would no longer match maya (his circles derive from his bonds), so the venue could not cross at all. Maya's membrane, meanwhile, would still cast raj exact; her circles derive from her bond, which stands. Trust is declared per party, per direction, and every consequence of it lives in the twin that declared it. That is Axiom III wearing arithmetic.

Related

• membrane, the audiences (family, team, others) that bonds populate.
• attention, the thresholds that bond-derived classes select.
• The pressure function, where T sits in the product.
• The v0.1 pragmas, the circles pragma in full.

assume / yield role, Semantic Addressing

A role declaration claims (or relinquishes) a named responsibility, so that other twins' membranes can address "whoever holds this role" instead of a person by name. Roles are the language's answer to forwarding chains, to stale org charts, and to the "who owns this now?" email thread: the pipe rebinds, and nobody gets notified, because nobody needs to be.

Syntax

From spec §5:

roledecl    = ( "assume" | "yield" ) "role" rolename ;
rolename    = ident "(" [ arg { "," arg } ] ")" ;

For example (spec §4.9):

assume role decision-owner(atlas.budget)

Semantics

Spec §4.9: a twin claims a role with assume and relinquishes it with yield. Roles matter because membranes may target role parties rather than named twins; the party production includes @role(rolename), as in the example rule of spec §4.7:

status(atlas.*) -> @role(lead, atlas):  exact

read as: anyone currently attested as lead of atlas may receive my atlas status facts at exact granularity, whoever that is at flow time.

The deeper design comes from the Osmosis Protocol spec §7. The mesh maintains a role registry binding attested roles ("decision-owner: Atlas budget") to membranes, with bindings signed by the parties entitled to confer them. A flow directed at a role resolves against the registry at the moment the flow fires, not at the moment the rule was written. Handoffs, reorganizations, and delegation therefore require no notification to any counterparty: the binding changes, and every membrane rule that targets the role follows it silently.

Honesty: v0.1 does not implement roles

Roles are specified language, not implemented language. Be precise about this if you are building on v0.1:

• The reference interpreter parses no roledecl. A line like assume role reviewer(atlas) is an unrecognized declaration and fails the parse. This is why dinner.osmol deliberately omits the assume role reviewer(atlas) line that appears in the spec §8 program. The shipped example is the §8 mesh minus the one construct v0.1 cannot read.
• @role(...) parties do parse inside membrane rules (the rule grammar accepts them), but they never match any audience: the interpreter's audience check knows family, team, others, all, and literal twin names, and an @role(...) party falls through to a literal name comparison that no receiver satisfies. A role-targeted rule is, in v0.1, a rule that grants nothing.

What roles wait on is the role registry, specified as one of OMP's four control message types (role-registry queries); this puts full role support on the wire roadmap rather than in the single-process interpreter. See The Wire Ahead. An implementation may parse and store role declarations today (that much is pure front-end work, and osmol check should accept them), but honest resolution of @role(...) requires an attested registry to resolve against.

Why this construct exists at all

It would have been simpler to leave addressing to names and groups. But endpoint addressing is one of the original pathologies, present already since 1971: mail goes to a mailbox identifier, not to the party who actually holds the decision, and humans spend their lives forwarding around the difference. Semantic addressing moves that resolution into the mesh, where it can be attested, signed, and current. assume/yield is the twin-side half of that promise; the registry is the mesh-side half.

Related

• membrane, where @role(...) parties appear as flow-rule targets
• stake, the other §4.9 posture construct
• The Wire Ahead, OMP control messages, including role-registry queries

stake, Priced Strangers

Syntax

stake = "stake" number "on" fact "toward" party ;

Example, from spec §4.9:

stake 5 on offer(design-review) toward maya

Semantics

In Osmol, flow requires a gap: no construct may create pressure toward a twin that has not declared a matching seek. That is error[O-003], no gap, no gradient. stake is the sole exception. It is the only construct that may originate pressure toward a twin holding no matching gap, and it does so by putting the initiator's reputation on the table.

The mechanics, per spec §4.9: the stake is forfeited if the receiver marks the flow unwanted, and returned with standing if the receiver adopts the gap. The spec's summary line is the whole design in one sentence:

Spam is thus not filtered by Osmol; it is priced by its grammar.

The economics

The stake mechanism is the language-level face of the Osmosis protocol's anti-spam economics (protocol spec, §8). Under that regime, bulk unsolicited contact carries linear cost and superlinear reputational risk: every stranger you press on costs a stake, and every "unwanted" verdict compounds against your standing. The spam strategy is not filtered but priced out of rationality. This inverts, at the protocol layer rather than the client layer, the economics email fixed in 1971, where sending is free and the receiver pays with attention.

The Fifty-Year Letter states both halves of the argument. The disease (its Chapter 2): an inbox is the only to-do list in your life that any stranger on Earth may write on, without permission, at no cost. Spam is a rational response to a broken price signal, not an abuse of it. And the sober rebuttal to the arms-race objection (its Chapter 7): sender agents will always be optimized against receiver agents, and the arms race already exists, but the attacker currently fights for free. You cannot stop adversaries; you can stop subsidizing them.

The formal version of this claim is Theorem 5 (Spam irrationality): under any strategy, the expected return of unsolicited pressure without adopted gaps is negative. It is game-theoretic, needs a different toolbox than the convergence proof, and is open; see The Open Theorems.

Honesty: v0.1 does not implement stake

The reference interpreter has no stake support at all. There is no rule for it in osmol.py's pattern table, so a stake line fails parsing as an unrecognized declaration: it neither prices nor flows. In v0.1, the only anti-spam machinery actually running is:

1. O-000, the tombstone verbs cannot be written, and
2. no-gap-no-flow, the engine only ever evaluates pressure against declared gaps, so a gap-less twin simply attracts nothing.

An implementer targeting v0.1 conformance should treat stake as reserved grammar with specified semantics awaiting a runtime: parse it if you wish to be forward-compatible, but do not invent flow behavior for it. The economics live in the wire protocol's future, not in today's interpreter.

Related

• O-003, Unsolicited Pressure, the wall through which this construct is a priced door
• seek, the gap, the only unpriced attractor of flow
• The Open Theorems, Theorem 5's status

The Grammar, Annotated

Osmol's grammar fits on one page, and that is not modesty, it is policy. A grammar small enough to hold in your head is also small enough to implement in a weekend and to audit in an afternoon. Two of the deepest guarantees of the language live not in any rule below but in the rules that are missing. This chapter reproduces the full EBNF from spec §5, walks through it production by production, and then looks at the absences.

The full EBNF

program     = { twin } ;
twin        = "twin" ident "{" { decl } "}" ;

decl        = hold | seek | owe | decide | express
            | membrane | attention | bond | roledecl | stake ;

hold        = "hold" fact "=" value [ "±" quantity ] [ "@" number ]
              [ [","] temporal ] ;
seek        = "seek" fact [ "by" instant ] [ "else" escalation ] ;
owe         = "owe" fact "to" party [ "by" instant ] ;
decide      = "decide" fact "among" "{" value { "," value } "}"
              [ "by" instant ] ;
express     = "express" "to" party ":" string ;

membrane    = "membrane" "{" { flowrule } "}" ;
flowrule    = selector "->" party [ "when" condition ] ":" transform ;

attention   = "attention" "{" { budget } "}" ;
budget      = "interrupts" nat "/" period
            | "quiet" timerange
            | "threshold" party number ;

bond        = "bond" party "{" "trust" level "}" ;
roledecl    = ( "assume" | "yield" ) "role" rolename ;
stake       = "stake" number "on" fact "toward" party ;

fact        = ident "(" [ arg { "," arg } ] ")" ;
selector    = fact | ident | "*" ;
party       = ident | "@role(" rolename ")"
            | "family" | "team" | "others" | "all" ;
transform   = "exact" | "coarse(" grain ")" | "category"
            | "existence" | "deny" ;
temporal    = "decays" ( instant | reltime )
            | "until" instant
            | "every" period ;
escalation  = "escalate" | "sync" | "drop" ;
condition   = fact comparator value | ident ;
value       = quantity | instant | place | ident ;
rolename    = ident "(" [ arg { "," arg } ] ")" ;
level       = "low" | "medium" | "high" | number ;

Production by production

program, twin. A program is a sequence of twins; a twin is a braced block of declarations, one per participant. There is nothing above the twin: no module system, no imports, no main. The twin is the compilation unit (Your First Twin), and since declaration order never matters (Axiom II), { decl } is in fact a set written with sequence syntax.

The ten decl kinds. Five speech acts: hold (assertion), seek (gap), owe (commitment), decide (decision), express (human-lane expression). Two sovereignty blocks: membrane (permissions as casts) and attention (the receiver's budget). Three postures: bond (trust), roledecl (assume/yield role, semantic addressing), and stake (priced unsolicited pressure). Note the optionality baked into the speech acts: by, else, ±, @, and the temporal clause are all bracketed, so the minimal forms, hold f(x) = v and seek f(x), stay one short line.

fact, selector, party, transform. A fact is an identifier applied to arguments, for example eta(dinner) or status(atlas.review), and dotted paths in idents give you hierarchies for free. A selector is a fact pattern for membrane rules, with * as the wildcard. A party is a named twin, a flow-time-resolved role, or one of the four audience classes. transform is the entire vocabulary of what a membrane may do (four downward casts and deny), and its shape is discussed under the absences below.

temporal, escalation, condition, value, rolename, level. The small vocabulary of knowledge physics: decays/until/every make validity part of the type; escalate/sync/drop are the three fates of a deadline-passed gap; conditions gate membrane rules on the twin's own state; values are quantities, instants, places, or idents; level grades a bond low/medium/high or numerically.

Grammar-versus-v0.1 gaps. The grammar is normative; the reference interpreter implements a documented subset. roledecl and stake are unimplemented; v0.1 rejects them as unrecognized declarations. when conditions on membrane rules parse but are never evaluated. Numeric levels in bond are not parsed (the interpreter's trust table knows only low/medium/high), and every in temporal is likewise unparsed. Every one of these gaps is listed, with its workaround, in the v0.1 pragmas; an implementation may honor them or consciously supersede them via RFC, but never silently diverge.

The load-bearing absences

Read the grammar again, this time for what is not there.

First, no production contains transmission. The word send appears on no right-hand side, and neither does any synonym, wrapper, or euphemism for it. There is no rule you can reach, no combination of productions you can compose, that yields "deliver this content to that party." The closest the grammar comes is express, which directs content to a party but still moves only by the mesh's settling, and stake, which prices the right to create pressure without a gap. Sending is not forbidden by a checker; it is unwritable.

Second, no production lets a seek, attention, or membrane name a foreign twin as its subject. Look at the rules: a seek has no party position at all, so you cannot seek at someone, only declare your own gap. attention and membrane are bare blocks with no owner argument; they attach to the twin whose braces they sit inside, and there is no syntax to point them elsewhere. The grammar can only speak about the twin it is inside.

As spec §5 puts it: the two deepest security properties of the system are enforced before type checking, by the shape of the syntax tree itself. Spam (O-003), attention theft (O-006), and wanting on someone else's behalf (O-001) are not policy violations that a checker must detect. They are sentences that cannot be parsed. The rest of the impossible sentences are cataloged in What Cannot Be Written.

For implementers

The engineering dissertation (Ch. 2) fixes the recommended front-end shape, and it is worth following even in a weekend port:

Lexing: handwritten and line-oriented. The grammar is line-oriented per spec §2, and a handwritten lexer gives the best diagnostic spans for a language this small; no generator earns its keep here. One deliberate theatrical choice is normative: the tombstone check runs at the lexer, before parsing exists. error[O-000]: there is no send should be the fastest error the toolchain can produce; the old world's verbs die at the first possible instant, before your parser has even seen a brace. (Strip string literals first: prose inside an express is payload, not a verb.)

Parsing: recursive descent, spans everywhere. Recursive descent over the EBNF above, producing a typed AST in which every node carries its source span. Parser combinators are acceptable; v0.1 recommends handwriting it, because the grammar is deliberately tiny and error recovery (parsing past a bad line to report many errors at once, rustc-style) is easiest to tune by hand. Spans on every node are not optional polish: in this language the error messages are the ethics, and ethics deserve line numbers.

Everything after the parser (the checkers, the lowering, the solver) is walked through in Implementing an Interpreter, with the 375-line reference as the map.

What Cannot Be Written

A language is defined as much by its impossible sentences as its possible ones.

(Osmol spec, §7)

Most language references catalogue what you can say. This section of the reference catalogues what you cannot, because in Osmol the impossible sentences are the point. The grammar was shaped so that the characteristic abuses of the 1971 paradigm have no spelling.

The design thesis

The spec §7 closes with the claim this entire section unpacks: in the old paradigm, spam, oversharing, attention theft, and impersonation were runtime problems, fought forever at the filter. In Osmol they are syntax errors, caught, in the spec's words, "at the only moment they are cheap: before existence."

A spam filter fights spam after it exists, forever, at the receiver's expense. A tombstone word fights it at the lexer, once, at the sender's compiler. The difference is not efficiency; it is who pays, and when, and whether the fight ever ends.

The errors are the ethics

The engineering dissertation (Chapter 2, semantic analysis) mandates that these diagnostics be rustc-grade: coded, spanned, and pretty-printed. Each code answers to osmol explain O-xxx with a paragraph of philosophy, "because in this language the error messages are the ethics." The seven chapters that follow this page are those paragraphs. When the Rust toolchain ships osmol explain, this is the text it should print.

The seven diagnostics

Enforcement in v0.1, honestly

The seven codes are all normative, their wording included, but they are enforced today by three different mechanisms, and an implementer should know which is which.

Mechanically enforced. O-000 fires in the reference interpreter at parse time: every line is scanned for tombstone words before any other processing (strings are exempt: prose is payload, and mentioning the word send inside an express is not sending). This is the one diagnostic you can trigger right now: run spam.osmol and watch it die loudly.

Enforced by grammar shape. O-001, O-003, and O-006 are impossible to write rather than illegal to run: no production lets a seek, attention, or membrane block name a foreign twin as its subject, and the engine only ever computes flows toward matching gaps. The spec §5 calls these absences load-bearing. The interpreter inherits the safety architecturally; there is simply no code path for the forbidden thing. Likewise O-004 and O-005: expressions bypass the membrane machinery entirely and carry provenance=human with no syntax to claim otherwise.

Awaiting the Rust checker. O-002 requires tracking each holding's granularity coordinate and rejecting upward casts; the v0.1 interpreter parses transforms but does not type-check the lattice. The explicit AST-level guards for O-001/O-004/O-005/O-006 (protecting against malformed trees constructed by tools rather than by the parser) are Stage 3 of the compiler pipeline, specified in the dissertation and due in osmol-core.

The distinction matters for anyone carrying the stone: a conforming implementation must produce all seven diagnostics, with these exact messages, from whatever stage can catch them earliest. The dissertation's instruction for O-000 is explicit: it fires at the lexer, because there is no send should be the fastest error the toolchain can produce.

O-000, Tombstone Verb

The error

error[O-000]: there is no send. Declare what you hold; declare what you seek; the mesh does the rest.

What fired

You used a tombstone word outside a string: one of send, notify, broadcast, blast, cc, bcc, forward, reply. These eight words are reserved in the grammar for exactly one purpose: producing this error. They have no other meaning, no production, no future. Strings are exempt: inside an express, prose is payload, and you may write about sending things as much as you want.

Why it exists

Axiom I: there is no send. The spec could have simply left the old verbs out of the reserved-word list, and any use would have died as an ordinary unrecognized-identifier error. Instead, spec §2 reserves them deliberately, "so that the old world's verbs die loudly rather than quietly." A language defines itself as much by its impossible sentences as its possible ones, and O-000 is the most impossible sentence of all; it got its own tombstone.

The ethics

The Fifty-Year Letter's autopsy of the inbox begins with inverted economics: sending is free, reading is expensive, the receiver pays. An inbox is a to-do list any stranger on Earth may write on at no cost, and spam is not an abuse of that system but a rational response to its broken price signal. Every one of the eight tombstoned verbs is a way of spending someone else's attention without their consent. Killing the verb kills the subsidy. The language does not fight free push at runtime with filters; it makes the push inexpressible at the only moment stopping it is cheap, that is, before it exists.

How to fix

The canonical must-fail program, spam.osmol, reproduced verbatim:

twin spammer {
  send offer(crypto) to everyone
}

The lawful rewrite declares what the spammer holds and, since no stranger has a matching gap, puts a priced stake behind the pressure (stake is the sole construct that may originate pressure toward a twin holding no matching gap):

twin spammer {
  hold offer(crypto) = available
  stake 5 on offer(crypto) toward maya
}

If the receiver marks the flow unwanted, the stake is forfeit. Spam is not filtered in Osmol; it is priced.

The notify instinct rewrites the same way, with the same two moves (supply on your side, demand on theirs):

-- old world: notify raj that the review is in progress
twin maya {
  hold status(atlas.review) = in-progress
}

twin raj {
  seek status(atlas.review)
}

Nobody notifies. Maya holds; raj seeks; the mesh does the rest.

In v0.1

The reference interpreter runs tombstone_check on every line before parsing it, stripping quoted strings first (payload exemption). This implements the engineering dissertation's Chapter 2 mandate: tombstones fire at the lexer, before a parser even exists, because error[O-000] should be "the fastest error the toolchain can produce". The old world dies at the first possible instant.

Running spam.osmol produces:

$ python3 -m osmol spam.osmol
OSMOL v0.1 - reference interpreter
osmol: line 2: error[O-000]: 'send' — there is no send. Declare what you hold; declare what you seek; the mesh does the rest.

The interpreter's message is slightly richer than the spec's: it prefixes the line number and the offending token ('send'), and it substitutes the caught word into "there is no X" (catch a notify and it says there is no notify). The spec §7 string at the top of this page is the normative one; the extra span information is only garnish, and a conforming implementation is expected to provide at least the code, the span, and the message class (see Conformance).

Related

• What Cannot Be Written: the six siblings of O-000.
• stake · hold · seek: the lawful vocabulary.

O-001, Foreign Gap

The error

error[O-001]: cannot want on maya's behalf. Gaps belong to their owners.

What fired

A seek naming another twin as its subject: an attempt to register a gap for someone else, from outside their twin.

Why the language forbids it

Axiom III: the receiver's grammar governs. A gap is the only thing in Osmol that attracts flow, which makes it the most consequential thing a twin can declare: it is standing permission for the mesh to route knowledge toward you. If any other party could register your gaps, they could manufacture your demand, and manufactured demand is the old push model in new clothes: "you wanted this", asserted by the person who benefits from you wanting it. Desire is sovereign. A system in which others can write your wants has only moved the inbox to a new place.

The grammar already enforces this structurally. Spec §5 notes, as one of its two load-bearing absences, that no production allows a seek (or an attention or membrane block) to name a foreign twin as its subject; the grammar can only speak about the twin it is inside. So why does the diagnostic exist? Because parsers are not the only producers of ASTs. Tools (code generators, migration scripts, LSP refactorings, anything that constructs syntax trees directly) can build shapes the concrete grammar cannot spell. The sovereignty checker in semantic analysis (dissertation Ch. 2, stage 3) exists to reject those shapes with O-001, so the property holds at the AST level and not only at the keyboard.

How to fix

Move the seek inside the twin that actually wants the value. There is no other fix, and that is intentional.

If what you really want is for them to learn something you know: declare the hold in your own twin and let their gap do the work. If they seek it and your membrane grants it, it flows. If they have no matching gap and you believe the knowledge matters anyway, stake reputation on it; that is the one lawful channel for unsolicited pressure. What you may never do is decide on their behalf that they want it.

In v0.1

The reference interpreter's line parser makes O-001 unenforceable-by-construction: a seek is always attributed to the enclosing twin, and the seek production has no slot in which a foreign twin could even be named. There is no code path that produces this error, because there is no way to write the offense. The explicit AST-level check lands with the Rust semantic analyzer, whose sovereignty checker guards against tool-constructed trees.

Related

• O-006, Foreign Sovereignty: the same axiom guarding attention and membrane
• seek · stake
• What Cannot Be Written

O-002, Granularity Inversion

error[O-002]: precision cannot be manufactured, only surrendered.

What fired

A membrane transform pointed upward along the granularity lattice. The spec's example (§7): a rule of the form -> others: exact where the holding itself is only known at coarse(city). The membrane was asked to emit more precision than it possesses.

Why the grammar forbids it

Axiom IV: precision only flows downhill. Every value carries a granularity coordinate on the lattice

exact ⊒ coarse(g) ⊒ category ⊒ existence

and the type system admits transforms only downward. Coarsening is a cast; refinement is a type error. There is no syntax for an upward cast (per spec §4.7, the grammar simply has no word for it), so O-002 exists to catch the one place where inversion can still be expressed: a membrane rule whose declared output grain exceeds the grain of the value flowing through it.

The ethics are the point. Privacy leaks are usually precision leaks: you shared your city and something downstream reconstructed your street. A system that can sharpen your data after you released it has taken something you never gave. In Osmol that sharpening is not a violation to detect, it is a sentence that cannot be typed: downstream of any membrane, information can only get blurrier.

How to fix it

You have exactly two honest options: surrender the precision, or stop promising it.

twin ana {
  hold location(ana) = grid(52.52, 13.40)   -- known only at coarse(city)
                                            -- (it arrived through a membrane at that grain)
  membrane {
    location(*) -> others: exact            -- error[O-002]: upward cast
  }
}

Either accept the coarser transform, so you promise no more than you hold:

  membrane {
    location(*) -> others: coarse(city)     -- ok: identity cast, M stays fractional
  }

or, if others genuinely need street-level truth, refine the source hold: obtain the value at exact yourself, at the origin, where the precision legitimately exists. What you may never do is write a rule that conjures the precision in transit.

In v0.1

This diagnostic cannot fire in the reference interpreter. osmol.py does not track a holding's granularity coordinate: values are opaque strings, and casts are applied only as pressure weights (exact 1.0, coarse 0.7, category 0.5, existence 0.3) plus a textual annotation on the delivered value. With no grain on the holding, there is nothing to compare a rule's output grain against.

The full lattice checker is Stage 3 (semantic analysis) work in the engineering dissertation's compiler pipeline. The corresponding runtime guarantee, Theorem 4 (Granularity monotonicity), which states that along any flow path granularity is non-increasing, is open. Implementers building beyond v0.1 should type every value as a (value, granularity) pair and reject upward casts statically; that single enrichment makes both O-002 and Theorem 4 checkable.

Related

• Granularity: the lattice, in full
• membrane: where casts are declared
• The Open Theorems: the status of Theorem 4

O-003, Unsolicited Pressure

The error

error[O-003]: no gap, no gradient. Stake reputation or remain silent.

What fired

A program constructed flow toward a twin that has no matching gap, outside a stake. Something tried to push where nothing pulls.

Why the language forbids it

Gaps are the only attractors in Osmol's physics (spec §3): the pressure function is evaluated over (holding, gap) pairs, so where there is no gap there is no gradient, and where there is no gradient there is nothing for a flow to be. This is Law I (receiver sovereignty) carried down into the type system, and it makes the Osmosis protocol's anti-spam economics (§8) grammatical: unsolicited pressure is simply not evaluated unless the initiator attaches a forfeitable reputation stake.

The ethics are inherited from the autopsy of email. "An inbox is the only to-do list in your life that any stranger on Earth may write on, without permission, at no cost." Fifty-five years of spam, cold outreach, and reply-all storms were rational responses to that broken price signal. Osmol does not filter the stranger. It makes the stranger pay, or stay silent. Spam here is not a runtime battle; it is a sentence the language refuses to parse for free.

How to fix it

Two legitimate paths, and only two:

1. The receiver declares the interest. If they actually want what you hold, the fix is on their side: a seek for the fact. Then a gradient exists and ordinary settling takes over.
2. You pay for the introduction. Write stake n on fact toward party, the sole construct that may originate pressure toward a gap-less twin. The stake is forfeited if the receiver marks the flow unwanted, and returned with standing if the receiver adopts the gap. Accept the forfeiture risk or reconsider whether this flow deserves to exist.

In v0.1

The reference interpreter enforces O-003 by engine shape rather than a raised error: the settle loop only ever iterates over receivers' gaps, pairing each with candidate holdings, so unsolicited flow is not rejected, it is unrepresentable. There is no code path in which a holding moves without a gap pulling it. stake itself is unimplemented in v0.1 (see stake and the v0.1 pragmas), so today the only strangers in the mesh are silent ones.

The formal claim behind all this is Theorem 5, spam irrationality: under any strategy, the expected return of unsolicited pressure without adopted gaps is negative. It is stated in spec §9 and remains open. See the open theorems.

Related

• seek: the gap, the only attractor.
• stake: the priced exception.
• O-001: you also cannot manufacture the gap on the receiver's behalf.

O-004, Transformed Expression

error[O-004]: the human lane is verbatim.

What fired

Any membrane or attention rule whose selector matches an express. It does not matter whether the rule meant to coarsen, summarize, delay, deny, or merely classify: if its selector can touch expressive content, it is O-004.

Why this is an error

Axiom V: the human lane is verbatim. The spec §4.6 defines express as the only construct admitting free prose: verbatim across the mesh, provenance-stamped, and immune to every transform and every attention rule. It may be queued by quiet hours; it may never be summarized or silenced. The Osmosis Protocol spec (§9) states the same rule from the protocol side: human-expressive content is routed to a reserved lane that the placement classifier is prohibited from silencing, and the lane is deliberately inefficient (no summarization, no batching, full fidelity).

The ethics: compression is for logistics. An ETA can be coarsened to the half hour and lose nothing that mattered. But affection, condolence, humor, and conflict have their value in their exact form. A summarized apology is not an apology, and a condolence rendered "at category granularity" is an insult with a type signature. The whole architecture exists to shrink every other lane so that this one can stay wastefully, humanly exact. A membrane rule that matches an expression is the system beginning to optimize the one thing it swore to leave alone.

How to fix it

Delete the rule. If your selector is a wildcard that by accident also catches expressions, narrow it to the fact families you actually mean to govern.

If what you want is to limit when expressive content can reach you, that is legal; use quiet:

attention {
  quiet 22:00-07:00
}

Quiet hours queue the lane; they never transform it. The fox note arrives at 07:00 exactly as it was written. What no grammar will ever give you is a selector on express, not to shorten it and not to mute a person's own words.

In v0.1

The reference interpreter enforces this axiom by architecture rather than by check: settle() delivers the human lane first, before any flow fires, and the delivery path never consults membrane_cast, so expressions structurally cannot meet a membrane. The explicit semantic-analysis check (rejecting a rule whose selector matches an expression, for AST-level construction by tools) is future checker work, specified for osmol-core's Stage 3. See What Cannot Be Written for the enforcement map.

Related

express · O-005, counterfeit humanity · The Five Axioms

O-005, Counterfeit Humanity

The error

error[O-005]: machines may not counterfeit the human lane.

What fired

An express authored by an autonomous process. Every expression carries mandatory authorship provenance, and the classes are exactly three (spec §3): human (the default), assisted (permitted, and disclosed), and autonomous, which is not so much forbidden as unrepresentable. There is no syntax for an autonomous express, just as there is no syntax for send. A toolchain that finds itself constructing one has left the language, and O-005 is the door it hits.

Why it exists

Axiom V: the human lane is verbatim. No transform may compress it, and no autonomous process may author it. This is Law V of the Fifty-Year Letter (Proven Provenance) meeting Law IV (Layered Actors) at their sharpest corner. The letter names the failure mode precisely: not too little communication, but the automation of intimacy. Its authorship-disclosure requirement exists "precisely so a birthday message ghost-written by a model cannot masquerade as a human act."

The ethics

The human lane is the one channel Osmol protects absolutely: verbatim across the mesh, immune to membranes, immune to attention rules, delivered first. That protection is only worth having if what arrives there is what it claims to be. Trust in the protected lane is the currency of the whole system: the reason a friend's words can bypass every filter is that they are known to be a friend's words. Counterfeit warmth debases exactly that currency, and unlike counterfeit logistics, it cannot be caught by checking facts. So the language refuses at the root: a machine with feelings to report has no grammar to report them in.

How to fix

An agent that has something to say does not say it. It holds it, and lets gaps pull. Machine-discovered information is logistics, and logistics has a lawful, provenance-honest vocabulary:

-- unwritable: an agent expressing warmth as its owner
-- express to mom: "Happy birthday! Thinking of you."   (autonomous author)

-- lawful: the agent supplies facts; interested twins draw them
twin maya-agent {
  hold birthday(mom) = 2026-07-19
  hold gift-status(mom.birthday) = shipped
}

Only humans write express. A human writing with disclosed machine help is the assisted class: permitted, because the disclosure is the point. The one thing that has no representation is a machine wearing a person.

In v0.1

The reference interpreter's grammar simply has no way to mark an express as machine-authored: every expression parsed from source is treated as human speech, and the human lane delivers it first, verbatim, stamped as such in the trace:

  human-lane  maya -> raj  (verbatim, provenance=human): "Saw a fox on the way home and thought of you."

So in v0.1, O-005 is enforced by unrepresentability alone. The diagnostic exists for toolchains that construct ASTs directly, and the provenance stamp is an honest label, not yet a verified one.

The real teeth are cryptographic, and they are on the roadmap, not in the interpreter. The engineering dissertation's Chapter 5 specifies that every delta is signed over payload ‖ provenance chain ‖ authorship class ‖ nonce, with keys held in platform secure hardware. That makes the authorship label a cryptographic claim, not metadata: forging "a human wrote this" becomes forging a signature. Until that layer ships (see the wire roadmap), the honest description of v0.1 is that the human lane is protected by grammar and labeled by convention, which is exactly as far as a single-process interpreter can carry Law V.

Related

• express: the one construct of the human lane.
• O-004: the transform half of Axiom V.
• The wire roadmap: where signatures make provenance real.

O-006, Foreign Sovereignty

The error

error[O-006]: thresholds belong to receivers. This is the entire point.

What fired

A reference to another twin's attention or membrane: any construction that reads, lowers, spends, or otherwise touches the sovereign machinery of a twin from outside it.

Why the language forbids it

Axiom III, at full strength. Spec §4.8 is explicit that budgets and thresholds are legal only inside the twin they govern, and that referencing another twin's attention block "is not a permission error at runtime; it is a parse-impossible construction." Spec §5 counts this among its two load-bearing absences: no production allows an attention or membrane block to name a foreign twin as its subject. The Osmosis Protocol spec §3 states the underlying law of the pressure engine:

The threshold is the receiver's property; no sender may lower it.

This is the founding inversion of the whole project. For fifty years already, the ambient economics of communication have subsidized free access to strangers' minds: anyone could place an item on your attention at no cost to themselves, and the entire defensive apparatus (filters, folders, do-not-disturb, inbox-zero rituals) lived on your side, at your expense, forever losing. Law I (Receiver Sovereignty) ends the subsidy, and O-006 is where the ending is enforced. Note how little it would take to undo this: a single construct that lets a sender adjust a receiver's threshold, one line of grammar, rebuilds the inbox. Every "priority" flag, every "urgent" subject line, every notification a sender could force through was exactly that construct in the old world. The language refuses to contain it.

How to fix

You cannot, and that is the point. There is no rewrite of a foreign-sovereignty reference that preserves its intent, because the intent, reaching past someone's declared bar, is exactly the thing being forbidden.

What you can do instead, all of it on your own side of the membrane: declare better holds, so that when their gaps form, your supply is the relevant match; earn trust over time, since a receiver who bonds you moves you to a friendlier sender class with a lower threshold (their choice, made in their source); or stake reputation on genuinely valuable unsolicited knowledge. The receiver's bar stays theirs in every case.

In v0.1

Structurally unwritable: the reference interpreter's parser only ever attaches membrane and attention blocks to the enclosing twin, and no parsed form can name another twin's blocks. As with O-001, the explicit AST-level guard is dissertation Ch. 2 stage 3 work (the sovereignty checker in the Rust semantic analyzer), defending against trees constructed by tools rather than typed by hands.

The formal counterpart is open. Theorem 3 (Attention soundness), which states that interrupt placements at a twin never exceed its declared budgets for any behavior of any other twin, is the machine-checked version of "this is the entire point," and it has not been proven yet. See The Open Ledger.

Related

• O-001, Foreign Gap: the same axiom guarding seek
• attention · membrane · bond
• What Cannot Be Written

The Pressure Function

Everything the mesh does reduces to one scalar. For every linked pair where A holds a fact and B has a gap it might close, the engine computes a pressure. The maximal pressure that clears its receiver's threshold fires as a flow, the flow closes the gap, and this repeats until nothing clears anything. That final quiet we call equilibrium. On this page we look at the anatomy of the scalar.

The equation

From spec §6, verbatim:

P(A→B, k, g) = R(k, g) × U(g, t) × T(A, B) × M(A→B, k) − C(B, t)

A flow fires iff P > θ_B(A), where the threshold is the one the receiver declared for that sender class.

Four multiplicative terms and one subtraction. The shape is itself the argument: relevance, urgency, trust, and permission multiply, so any one of them at zero annihilates the flow. A denied membrane (M = 0) cannot be overcome by any amount of urgency. Attention cost subtracts, so a tired receiver raises the bar for everyone at once.

Term by term

R, semantic relevance of the holding k to the gap g. In the full protocol this is embedding similarity over a vector index (Osmosis spec §3): "weather in Berlin" should attract a holding that is labeled differently but means the same. In v0.1 the interpreter only pairs identical fact names, so R is constant 1.0.

U, urgency, a function of the gap's deadline and the holding's decay. v0.1 pragma: 1.3 if the gap declares a deadline (by ...), else 1.0. No wall clock is simulated, so urgency does not yet grow when a deadline comes closer.

T, trust: the weight of the receiver's bond toward the sender, that is B's declared confidence in A, not the reverse. v0.1 weights: high = 1.0, medium = 0.6, low = 0.3; an undeclared bond defaults to 0.6.

M, membrane passage: what A's membrane grants for this fact toward this receiver. 0 for deny, 1 for exact, fractional under coarsening. v0.1 weights: exact = 1.0, coarse(...) = 0.7, category = 0.5, existence = 0.3, deny = 0.0. Also, no matching rule at all means no flow, before pressure is even computed.

C, attention cost at B: a function of B's interruption budget, focus state, and local time (Osmosis spec §3). v0.1 pragma: 0.0 always, because there is no wall clock, so there is no "now" to be busy in.

The threshold is the receiver's property

θ_B(A) is declared in B's own attention block, per sender class, and defaults to 0.3 for family, 0.4 for team, 0.8 for others. This is Axiom III made arithmetic: thresholds, budgets, and quiet hours are properties of the receiving twin, declared in the receiving twin's source, and no construct in any other twin's source can reference, lower, or spend them; attempting it is error[O-006]. A sender can raise its own pressure only through legitimate terms (a real deadline, an earned bond, a generous membrane of its own); the bar itself belongs entirely to the receiver.

Determinism

The engineering dissertation (Chapter 1) fixes a rule that this book treats as spec-level: among fireable flows of equal pressure, order lexicographically by (sender name, receiver name, fact). Given the same declarations and the same injected human judgments, every conforming solver must therefore produce the identical flow trace on every platform. That single rule is what makes golden-file testing, differential testing between implementations, and cross-mesh audit possible, because a trace is evidence only if it is reproducible.

Honesty note, a documented conformance gap. The v0.1 Python interpreter fires the maximal-pressure flow, but among ties it keeps the first candidate found in iteration order (twin declaration order), not the lexicographic rule. In the dinner mesh below, flows t1 and t2 tie at P = 1.30; the lexicographic rule orders (maya, raj, eta(dinner)) before (raj, maya, venue(dinner)), yet the Python engine fires raj's venue first because maya's gap is scanned first. The Rust core must implement the lexicographic rule; the conformance suite will encode it; the Python engine's trace order is, on this one point, not normative.

Worked arithmetic: the dinner mesh by hand

Run the dinner mesh and the trace prints its own arithmetic:

t1  raj.venue(dinner) --exact--> maya   P=1.30 (R1.0*U1.3*T1.0*M1.0) > theta[family]=0.3   [ledger]
t2  maya.eta(dinner) --exact--> raj   P=1.30 (R1.0*U1.3*T1.0*M1.0) > theta[family]=0.3   [silent]
t3  maya.status(atlas.review) --category--> raj   P=0.65 (R1.0*U1.3*T1.0*M0.5) > theta[family]=0.3   [silent]

Recompute each:

t1, venue to maya. Maya seeks venue(dinner) by 18:00: a deadline, so U = 1.3. Maya bonds raj trust high, so T = 1.0. Raj's membrane grants venue(*) -> family: exact, so M = 1.0. P = 1.0 × 1.3 × 1.0 × 1.0 − 0 = 1.30. Maya's threshold for raj: raj is family-class (she bonds him high) and she declared no family threshold, so the default 0.3 applies. 1.30 > 0.3, so the flow fires. The gap carried else escalate, so placement is ledger.

t2, eta to raj. Raj seeks eta(dinner) by 19:00: U = 1.3. Raj bonds maya high: T = 1.0. Maya's membrane: eta(*) -> family: exact (raj is in her family circle by bond), M = 1.0. P = 1.30 > θ[family] = 0.3, so a flow, silent.

t3, status to raj. Raj seeks status(atlas.review) by thu: U = 1.3. T = 1.0 as before. Maya holds status(atlas.review) (auto-emitted by her owe, a v0.1 pragma), and her membrane grants status(*) -> team: category, so M = 0.5. P = 1.0 × 1.3 × 1.0 × 0.5 = 0.65 > 0.3, so a flow, silent, delivered class-level: raj's twin learns in-progress, not the details.

Three flows, and the engine stops: no holding matches a gap any longer, no pressure clears any threshold. Silence is a fixpoint, and Theorem 1 proves the stop always comes.

Related

• Equilibrium: what the fixpoint is
• Granularity: where M's fractions come from
• attention · bond · membrane: the constructs behind θ, T, and M
• The v0.1 Pragmas: every simplification above, in one list

The Granularity Lattice

Every value in Osmol carries a second coordinate alongside its content: how sharp it is. Axiom IV (precision only flows downhill) turns that coordinate into a one-way street, and this chapter is the map of that street.

The lattice

exact ⊒ coarse(g) ⊒ category ⊒ existence

exact         19:40 ±5m                     the value as held
  │ cast
  ▼
coarse(g)     ~19:40, to the half hour      rounded to a declared grain
  │ cast
  ▼
category      "evening"                     only the class of the answer
  │ cast
  ▼
existence     an ETA exists                 only that a value exists

Four rungs. exact is the value as held. coarse(g) is the value rounded to a declared grain: coarse(30m), coarse(city), coarse(week). category keeps only the class of the answer. existence says only that a value exists at all. Every value type (quantity, instant, place, enum, entity) carries a granularity coordinate, and the full type of an assertion is the triple (value type, granularity, temporal validity).

Movement down the lattice is a cast: legal anywhere, meaning-preserving in the only direction that can be honest. Movement up is a type error, because refinement would mean manufacturing information the source never surrendered. The grammar cooperates by having no word for it (the membrane transform vocabulary contains only the four rungs and deny), and the checker backstops it with O-002: precision cannot be manufactured, only surrendered.

Casts in flight

Membrane transforms are the cast mechanism: each flow crosses the sender's membrane and is cast to the rule's grain on the way through. The cast also prices the flow. Inside P = R × U × T × M − C, the factor M is the cast weight: exact 1.0, coarse(g) 0.7, category 0.5, existence 0.3, deny 0. Coarser knowledge exerts less pressure, which is exactly right: a city-grain location rarely justifies interrupting anyone.

The v0.1 interpreter renders casts textually in apply_cast: exact passes the value through unchanged; coarse renders ~value [coarse(30m)]; category renders value [class-level]; existence renders [exists]. You can see two of these in the real dinner trace:

t2  maya.eta(dinner) --exact--> raj   P=1.30 (R1.0*U1.3*T1.0*M1.0) > theta[family]=0.3   [silent]
t3  maya.status(atlas.review) --category--> raj   P=0.65 (R1.0*U1.3*T1.0*M0.5) > theta[family]=0.3   [silent]

After t2, raj's twin holds 19:40 ±5m, exact, because raj is family. After t3 it holds in-progress [class-level], that is the review's status at category grain, with M = 0.5 visibly discounting the pressure. And if raj were not bonded trust high by maya, her second membrane rule (eta(*) -> others: coarse(30m)) would match instead, and his twin would absorb ~19:40 ±5m [coarse(30m)]: the same fact, honestly blurred.

What is not yet proven

Theorem 4 (granularity monotonicity) states that along any flow path, granularity is non-increasing: no composition of casts refines information, even across multi-hop flows through several membranes. It is stated in spec §9 and it is open. The Theorem 1 machine-check (the certificate) abstracts membranes into a boolean oracle, so it says nothing about grains; enriching the oracle back into explicit casts, with facts as (value, granularity) pairs, is the identified route to formalizing Theorems 2 and 4 in the same framework; see the open theorems.

Honesty about v0.1, likewise: the reference interpreter does not track granularity coordinates on holdings. Values are uninterpreted strings, and the cast markers above are renderings, not typed grains. So O-002 cannot yet fire mechanically; nothing in the engine knows that coarse(city) is below exact. A conforming implementation that types the lattice for real would be a major, welcome step past the reference.

Who defines coarse(city)?

The lattice's shape is fixed by the spec. Its grains are not: what counts as coarse(city) for a location, coarse(week) for a date, coarse(band) for a salary, differs by domain and by jurisdiction, and spec §10 is plain about what that means: who defines a grain per domain is a standards question, and standards questions are political questions wearing file formats.

The planned venue for those politics is the Lattice Registry, the governance-flavored appendix of the documentation site sketched in the engineering dissertation (Ch. 9). It defines standard granularity lattices per domain, so that two independent implementations coarsen the same value the same way. It does not exist yet. If you have a domain whose grains you understand (logistics, medicine, payroll), a registry entry is a good first RFC: it is small and concrete, and everyone who comes after will build on it.

Equilibrium and the Small-Step Relation

This chapter is the formal heart of the book: what an Osmol program is once the parser is done with it, how the mesh moves, and why it always stops. If you are implementing a solver, everything you must preserve is on this page; everything you may vary is not.

Deployment, not execution

An Osmol program does not run. Per spec §6, it is deployed: the compiler emits three artifacts, a typed state schema for the on-device model, a membrane policy set installed into the participant's edge membrane object, and gradient triggers registered with the mesh. Source never executes; it is not even present at runtime. What evaluates is the mesh, continuously and event-driven, over the deployed state of every participant.

This is the deepest consequence of Axiom II. Because programs are claims rather than commands, there is no program counter, no call stack, no "current line." The only dynamics the language has are the dynamics of pressure between declared states. So the semantics is small enough to fit in one rule.

The small-step relation

The mesh evaluates the pressure function P = R × U × T × M − C over every linked pair where A holds k and B seeks g. A flow fires iff P > θ_B(A). When it fires, it synthesizes an understanding-delta δ (the minimal signed assertion, cast to the membrane's granularity) and B absorbs it. The spec §6 gives the step rule:

⟨S_A, S_B⟩  ──[ P > θ_B ]──▶  ⟨S_A, S_B ⊕ δ⟩      where gap(g) ∉ S_B ⊕ δ

Read the side condition carefully: absorbing δ closes the gap. The closing is the definition of a step, not an optimization. Also note what the rule does not touch: S_A appears unchanged on the right. Flows are not transfers; A loses nothing, and B's state only grows.

Absorption is monotone: deltas only close gaps and add assertions; nothing un-knows. Transforms are monotone too, but downward: every membrane cast moves a value down the granularity lattice, never up (Axiom IV). Two monotone directions, one for knowledge and one for precision, and no rule in the system violates either.

The Datalog family

Monotonicity is not a style choice. It is what buys termination. A finite fact base evolving under monotone rules is exactly the setting of Datalog, and it inherits Datalog's central theorem: evaluation reaches a least fixpoint in finitely many steps. The spec names that fixpoint equilibrium, and calls it the halting state of every Osmol mesh between external events.

The argument, in short: the mesh starts with finitely many gaps; every step closes exactly one and creates none; therefore no run of the step relation can be longer than the initial gap count. Equilibrium is the state where no pressure clears any threshold, either because every gap is closed, or because what remains open is priced above what any sender's standing can reach. Both are stable. Both are success. A mesh with no gaps at all admits no step whatsoever: silence is a fixpoint.

External events (a new declaration, a decay firing, a human judgment injected into a decide, legacy email arriving through the adapter) perturb the state, and the solver settles again. The life of the mesh is therefore a sequence of settlements punctuated by the world. The spec has a line we should keep whole: "Communication, in this model, is what settling looks like from the inside."

The full formal treatment, with the machine-checked proof, is in Theorem 1.

Placement

Settlement decides what B now knows; placement decides what B's owner sees. Each absorbed delta is classified into one of three placements (spec §6):

• silent: the state updates; nothing renders. This is the majority case: the participant simply possesses current knowledge on next reference.
• ledger: the delta surfaces on the consequence-sorted board of commitments, decisions, and open questions, without interruption.
• interrupt: the delta renders now, debiting the sender-class budget declared in the receiver's attention block.

Expressions bypass classification entirely into the human lane, subject only to quiet, the one channel that placement may delay but never touch (O-004).

The Osmosis Protocol spec (§6) specifies the fuller mechanics this classification grows into: interruption budgets denominated per link and per period, chronic overdraft raising the effective θ for that sender, and interruption-class deltas required to carry a declared consequence-if-ignored field verified for plausibility. That machinery is protocol-future: the language reserves its place; v0.1 implements the three-way classification only (see the pragmas).

The solver shape

The step relation says what a step is; it deliberately does not say how to find one. The engineering dissertation (Chapter 3) fixes the reference shape: the solver is event-driven with a fixpoint sweep. Any state change at either end of a link enqueues gradient evaluation; the loop then fires the maximal-pressure flow, applies the membrane cast, absorbs, and repeats until no pressure clears any threshold. Among fireable flows of equal pressure, order lexicographically by (sender, receiver, fact); this is the determinism rule that makes golden traces possible across implementations.

Decays and deadlines enter as a monotone clock parameter: the clock perturbs urgency, and each perturbation may allow new settling, but between perturbations the convergence argument is untouched, because the clock never un-closes a gap. This is why "event-driven" is safe: there is no schedule the solver could choose, no interleaving it could pick, that breaks termination. Fire any fireable flow in any order and the mesh still finds the floor; fire the maximal one in tie-broken order and every implementation finds the same floor, step for step.

That is the entire contract a solver must honor: monotone absorption, downward casts, receiver-owned thresholds, maximal-pressure selection with the lexicographic tie-break, and the runtime assertion that flows never exceed the initial gap count. Everything else (data structures, scheduling, habitat) is yours.

Why the loop must terminate is no longer an argument in prose. It is a theorem, checked by a machine that cannot be persuaded. The next chapter is its certificate: Theorem 1.

Theorem 1, Convergence, Machine-Checked

The claim

Spec §9 states it in one sentence:

Theorem 1 (Convergence). Every finite mesh with no external input reaches equilibrium in finitely many steps.

This is the theorem the whole design leans on. A language whose runtime is "keep flowing until nothing flows" is only a language if the flowing stops. For Osmol it does. And unlike Theorems 2-5, which remain open obligations, this one is no longer a claim. It is machine-checked.

What the machine certifies

The proof lives in osmol_convergence.v, checked by Coq 8.18.0, accepted on the first compile. Three statements are certified:

• convergence: the osmosis step relation is well-founded, so there exists no infinite sequence of flows. Every finite mesh, left without external input, settles. Equilibrium is not a hope of the design but a mathematical necessity of it.
• chain_bound: the quantitative version. A mesh whose twins carry g open gaps in total reaches equilibrium in at most g flows. So settling is bounded by the amount of unmet demand, and by nothing else.
• zero_is_equilibrium: a mesh with no open gaps admits no flow at all. Silence is a fixpoint, not a failure. A quiet phone is the system working.

The file ends with Print Assumptions on all three theorems, and Coq's answer is Closed under the global context: zero axioms, zero Admitted. The verifier itself reports that nothing was assumed.

The model, and the honesty block

Machine-checked does not mean the whole language is proven, and this section is the mandatory fine print. The .v file carries its own honesty block in its header; here is what it says, restated without softening.

A twin, in the model, is a pair (holds, gaps): the assertions it possesses and the absences it seeks. That is all. Membrane, trust, urgency, and threshold are folded into a single boolean oracle allowed a b k, read as "the membrane grants a→b on k, and the pressure clears b's threshold." The theorem is then quantified over all oracles: convergence is proven for every possible membrane policy, pressure formula, and attention budget at once, including adversarial ones. This is a strengthening, not a cheat: a property that holds for every oracle certainly holds for the one your implementation computes.

But it means, equally, that the proof is over the flow bookkeeping, not the pressure arithmetic. Nothing in the certificate checks that P = R × U × T × M − C is computed correctly, that thresholds are compared correctly, or that membranes cast correctly. What is checked is the skeleton those computations hang from: a flow requires a holder, a seeker, and a grant; its sole effect is to close one gap and add one holding; no rule creates a gap.

Finally, the theorem's own precondition, "no external input", is encoded structurally: the step rule is the only rule in the system. A real mesh is perturbed continuously by new declarations, decays, and (someday) arriving legacy email. What the theorem guarantees is that between perturbations, the solver always finds the floor. It never oscillates and never runs away.

A guided read of osmol_convergence.v

The file is under a hundred lines of actual proof, and you can read it in full in one sitting. The tour:

The universe. fact is nat (facts drawn from a countable universe, without loss of generality), with decidable equality (fact_eq_dec).

The records. twin is { holds : list fact ; gaps : list fact }. mesh is a list of twins plus the oracle: allowed : nat -> nat -> fact -> bool, indexing sender and receiver by position.

The measure. total sums gap-list lengths across twins; gapcount m is the mesh's total open demand. This single number is the proof's fuel gauge.

The step. One inductive, one constructor:

Inductive step : mesh -> mesh -> Prop :=
| flow : forall (m : mesh) (a b : nat) (A B : twin) (k : fact),
    nth_error (twins m) a = Some A ->
    nth_error (twins m) b = Some B ->
    In k (holds A) ->
    In k (gaps B) ->
    allowed m a b k = true ->
    step m (Mesh (replace (twins m) b
                    (Twin (k :: holds B)
                          (remove fact_eq_dec k (gaps B))))
                 (allowed m)).

Twin a holds k, twin b seeks k, the oracle grants it; the effect at b is that gap k closes and holding k appears. Nothing else moves. This is spec §6's monotone absorption, and the absence of any second constructor is "no external input."

Two lemmas of list surgery. remove_lt: removing a fact that is present strictly shortens the list, so absorption really closes something. total_replace_lt: replacing one twin with a twin of strictly fewer gaps strictly lowers the mesh total.

The heart. step_decreases : step m m' -> gapcount m' < gapcount m. Every flow strictly reduces total open demand. Notice what this lemma is: the axiom the language was built on (absorption is monotone; deltas only close gaps), now arriving as the engine of the proof. The spec's promise and the proof's engine are the same sentence.

The theorems. convergence is well_founded (fun m' m => step m m'), obtained by mapping meshes into ℕ via gapcount (well_founded_lt_compat): no infinite descending chain of flows can exist because no infinite descending chain of naturals does. chain_bound inducts over any chain of n flows to get n <= gapcount m. zero_is_equilibrium inverts a hypothetical step out of a zero-gap mesh into a contradiction: the seeker's gap list must be simultaneously empty and inhabited.

The sanity demo. The file closes with the maya/raj mesh from spec §8, distilled: fact 1 stands for eta(dinner); maya = Twin [1] [] holds it, raj = Twin [] [1] seeks it, the oracle says yes to everything. Checked examples: gapcount m0 = 1, a flow exists, and by chain_bound, equilibrium in at most one flow.

The audit. Three Print Assumptions commands: trust, but verify the verifier.

Reproduce it yourself

From the certificate, verbatim:

apt-get install coq        # Coq 8.18+
coqc osmol_convergence.v   # exit code 0; prints the assumption audit

The proof is not a PDF that asks for your confidence. It is a program whose type checker cannot be persuaded, and you can run it on the bus.

The runtime shadow of the proof

Theorem 1 has one more life: as an assertion in every implementation. The reference interpreter's settle loop carries it inline:

assert flows <= g0, "Theorem 1 violated — impossible"

where g0 is the initial gapcount, and every trace prints the bound and its verdict (EQUILIBRIUM after 3 flows (Theorem 1 bound 3: respected)). The engineering dissertation makes this a non-negotiable of the core, in every habitat: the proof guarantees the assertion cannot trip; "shipping the assertion anyway is how an implementation confesses instantly" if it ever betrays the semantics. A solver that trips it has not found a bug in the mathematics. It has proven, at runtime, that it is not implementing Osmol, which is precisely the kind of self-incrimination a conformance-governed language wants built in.

Related

• Equilibrium: the semantic model the proof distills.
• Open Theorems: Theorems 2-5, honestly labeled as open.
• Conformance: how the bound becomes a dynamic test on random meshes.

The Open Ledger: Theorems 2-5 and Open Problems

Theorem 1, convergence, is machine-checked. Nothing else is. This chapter is the honest frontier: the four theorems the specification declares but no one has proven, and the open problems the specification names but does not solve. If you want to contribute mathematics to Osmol, this page is the job board.

Four theorems, still open

The statements below are quoted verbatim from spec §9, which declares them as proof obligations for the formal phase, "suggested vehicle Lean 4 or TLA+ over the small-step semantics of §6." The Theorem 1 certificate adds a third natural vehicle: continuing in Coq, where the existing proof lives. Its closing ledger also sketches the route to each; those routes are reproduced with each theorem below.

Theorem 2 (Non-interference). No delta derived from twin A's state reaches twin B unless a membrane rule of A grants it. (Security: M = 0 annihilates P; grammar forbids foreign membranes.)

Status: OPEN. Why it matters: this is the privacy guarantee. An implementer who honors it can promise a user that deny means deny: not "filtered with high probability" but "no derivation exists." Route: formalizable in the existing framework by enriching the abstract oracle back into structure, with membranes as explicit casts, so that the grant is a syntactic object the proof can case on rather than an opaque boolean.

Theorem 3 (Attention soundness). Interrupt placements at twin B never exceed B's declared budgets, for any behavior of any other twin. (Receiver sovereignty as an invariant, not a courtesy.)

Status: OPEN. Why it matters: this is O-006's promise made adversarial, that is receiver sovereignty holding against any sender strategy, not just polite ones. An implementation's interrupt classifier can only be audited against a stated invariant, and this is that invariant. Route: needs a placement layer on top of flows. The current model stops at absorption and never formalizes silent/ledger/interrupt classification, so the layer must be built before the theorem can even be stated in the proof assistant.

Theorem 4 (Granularity monotonicity). Along any flow path, granularity is non-increasing. (No composition of casts refines information.)

Status: OPEN. Why it matters: single casts going downhill is a local check (O-002); this theorem is the global closure: no composition of casts across multi-hop paths can ever reconstruct precision a membrane surrendered. Multi-twin relay is exactly where an implementer's intuition is weakest. Route: the same enrichment as Theorem 2, facts as (value, granularity) pairs, casts as lattice operations, then an induction along paths.

Theorem 5 (Spam irrationality). Under any strategy, expected return of unsolicited pressure without adopted gaps is negative. (Game-theoretic; the stake mechanism of §4.9.)

Status: OPEN. Why it matters: the anti-spam story is economic, not filter-based. stake prices unsolicited pressure instead of blocking it, and this theorem is the claim that the pricing actually works against a rational adversary. Route: game-theoretic, and the certificate is frank that it "wants a different toolbox", that is expected-utility arguments over sender strategies, not fixpoint induction. It may be the last one to fall.

One reassurance from the certificate's ledger, and it should be repeated to anyone sequencing work: none of them block Phase 3. Prototypes, the Rust core, and the wire can all proceed while these remain open: the theorems harden claims the design already makes; they do not gate the design.

Open problems

Spec §10, the specification's own honest section, names five problems that are not theorems awaiting proof but designs awaiting a designer:

• Retraction. drop lapses a gap, but un-asserting a hold that has already equalized requires revocation-deltas, and their semantics are deferred. Monotone absorption ("nothing un-knows") is the engine of Theorem 1; retraction must be added without breaking it.
• Conflicting holds. Two twins holding contradictory values for the same fact resolve today by provenance weight and recency. A principled belief-merge is open.
• Truthfulness staking. Assertions carry confidence, but a staking mechanism for truthfulness (forfeit on falsification) is sketched, not specified.
• Gap privacy. Seeking is itself revealing: registering a gap discloses what you lack. v0.2 must let membranes govern the visibility of gaps, not only holdings.
• Lattice governance. Who defines coarse(city) per domain is a standards question, and, as the spec puts it, standards questions are political questions wearing file formats.

How to claim one

Proofs and problem-solutions enter the language the same way everything else does: as RFCs, accompanied by conformance cases. A proof RFC should state the theorem over the spec §6 semantics, name its vehicle, include the checked artifact (as osmol_convergence.v set the precedent: zero axioms, zero Admitted, Print Assumptions clean), and, where the theorem constrains implementations, contribute the conformance programs that would catch a violator dynamically. A design RFC for the open problems follows the standard template: motivation against the five axioms, precise grammar and semantics, effect on spec and suite.

See The RFC Process for the mechanics and Conformance for what a good golden case looks like. The ledger is open; the stone doesn't rush, but it does accept new carving.

One Engine, Four Habitats

This part of the book is for the people the whole book exists for: implementers. If you will build Osmol in any language, on any platform, this chapter is the architecture doctrine you agree to. Not because the reference code says so, but because the doctrine is what keeps a one-implementation language from quietly becoming a one-implementation product.

Where truth lives

The most consequential decision for a young language is where its truth lives. Languages rot when their behavior is defined by whichever implementation someone happens to run. So Osmol's truth lives above any implementation, and GOVERNANCE.md fixes the authority order:

1. The conformance suite (when it exists): programs paired with required outcomes; see Conformance.
2. The specification (osmol-spec-v0.1), together with the machine-checked theorems that formalize it (osmol_convergence.v and successors).
3. The reference implementation, "which serves the two above and never overrules them."

Implementations, including the reference one, are servants of those, never masters; see Governance and Licensing for the constitutional wording. When you find the Python interpreter disagreeing with the spec, the interpreter is wrong. This book documents at least one such spot honestly (the tie-break gap).

The doctrine

One engine, four habitats. This is the whole doctrine in one line. A single Rust crate, osmol-core, written with no operating-system assumptions, contains the entire language: lexer → parser → AST → semantic analysis → diagnostics → lowering → equilibrium solver. It compiles three ways:

• native: the osmol CLI binary;
• wasm32: the browser playground and Cloudflare Workers;
• FFI via UniFFI: a linked library for Android and iOS.

No habitat gets its own solver. No habitat gets its own parser. Divergence between habitats is by definition a bug in whichever habitat disagrees with the conformance suite. The moment two habitats can legitimately disagree, there are two languages wearing one name. The doctrine exists to make that outcome unthinkable, not just discouraged.

Two non-negotiables

Whatever you build, in whatever language, two properties of the core are not up for negotiation.

Determinism. Given the same declarations and the same injected human judgments, the solver must produce the identical flow trace on every platform. This requires the tie-breaking rule the dissertation fixes at spec level: among fireable flows of equal pressure, order lexicographically by (sender name, receiver name, fact). Determinism is what makes golden-file testing, membrane audits, and cross-implementation trust possible.

The Theorem 1 runtime assertion. Every solver, in every habitat, asserts at runtime that the flows executed never exceed the initial gapcount. The proof guarantees the assertion cannot trip; still we ship it, because this is how an implementation confesses instantly if it ever betrays the semantics. The Python interpreter carries this assertion today; yours must carry it too.

Four runtime shapes

The runtime is the mesh, and the mesh is four deployment shapes of the same solver (dissertation, Chapter 3):

• Local (osmol settle): all twins in one process. This is today's Python behavior, preserved forever as the didactic and testing mode. Everything in the tutorial runs here.
• Duo (osmold): one daemon per twin on one machine or LAN, membranes speaking the wire protocol over localhost. This is the first true mesh, the first time a delta actually crosses between processes, and also the next real rung on the ladder. See The Wire Roadmap.
• Edge: one Cloudflare Durable Object per twin, running the same WASM build of osmol-core inside the Worker. The DO holds the twin's membrane policy, its outbound-permitted state slice, queued deltas for offline devices, and the append-only audit log. The edge executes the same solver bit-for-bit as the laptop.
• Device: osmol-core linked into the phone through UniFFI, holding the private model, with signing keys that never leave secure hardware. The phone is the twin's body.

Four shapes, one solver, one trace.

The build order

Chapter 11 of the dissertation sequences the work so that every step is demonstrable and no step waits on a later one. Honestly marked, as of this writing:

• Step 0, PyPI. Done. pip install osmol is real; the reference interpreter ships.
• Step 1, the osmol-core front-end (lexer, parser, checker, all O-diagnostics). Done when osmol check matches the Python interpreter's judgments on the conformance corpus. Ahead.
• Step 2, the Rust solver. Done when differential traces are byte-identical on the corpus. Ahead.
• Step 3, WASM plus the osmol.dev playground. The dinner mesh settling live in a browser textarea. Ahead.
• Step 4, duo mode over the wire protocol on localhost. Ahead.
• Step 5, edge mode. Durable Objects and the .odb deploy path. Ahead.
• Step 6, device mode. The Android library with hardware-held keys. Ahead.
• Step 7, LSP and editor polish, riding alongside everything after Step 1. Ahead.

Each step's definition of done is a conformance addition: the suite grows as the ladder climbs, so finishing a step and proving a step are the same act. There are zero users today and no network transport yet. The ladder is how both stop being true, one falsifiable rung at a time.

The toolchain target

The CLI contract implementers aim at is one binary, osmol, in the modern single-tool style of go and deno (dissertation, Chapter 6):

The reference interpreter implements only the heart of settle today. We do not hide that as a shortfall. It is the honest floor the rest of this part builds up from.

Related

• The Reference Interpreter: what exists today, exactly
• The v0.1 Pragmas: the documented simplifications any successor must honor or consciously supersede
• Conformance: how a language stays a protocol
• The Wire Roadmap: from one process to a mesh

Implementing an Interpreter: the osmol.py Walkthrough

This is the heart of Part IV. If you want Osmol in your language (Rust, Go, TypeScript, anything), the 375-line reference interpreter is your map, and this chapter walks it from end to end. Nothing in osmol.py is clever, and that is its virtue: it is the smallest honest implementation of the v0.1 semantics, small enough to port in a weekend and to audit in an evening.

Shape of the whole

One file, Python ≥ 3.9, standard library only. Three movements:

1. Parse. A line-oriented regex parser builds twins from source.
2. Model. Twins and their mesh: plain objects, no framework.
3. Settle. The equilibrium engine fires flows until nothing clears a threshold.

The file's header says the rest:

There is no send.
(grep this file: the word appears only in the tombstone list.)

That grep is a real conformance property. In your port, the forbidden verbs should appear exactly once, in the tombstone set that exists to kill them:

TOMBSTONES = {"send", "notify", "broadcast", "blast",
              "cc", "bcc", "forward", "reply"}

The model

A Twin is the whole of a participant's state. Compare the fields to the construct pages and you will find a one-to-one correspondence:

self.holds = {}        # fact -> value
self.gaps = {}         # fact -> {"by":..., "esc":...}
self.owes = []         # (fact, to, by)
self.decides = {}      # fact -> {"among":[...], "by":...}
self.membrane = []     # (selector, party, cond, transform)
self.attention = {"interrupts": None, "quiet": None, "theta": {}}
self.bonds = {}        # party -> trust
self.expressions = []  # (to, text)
self.ledger = []
self.lane = []         # human lane, verbatim

A Mesh is just twins plus one method: gapcount(), the sum of open gaps across all twins. That number is sacred. It is the quantity Theorem 1 proves strictly decreasing (every flow closes exactly one gap), so the initial gapcount is a hard ceiling on how many flows can ever fire. The engine measures it once, prints it, and enforces it (below).

Parsing

The parser is a table of regexes, RX, one per declaration form, applied line by line. Before anything else, each line is stripped of comments (-- to end of line) and handed to tombstone_check first, with string literals removed, because prose inside an express is payload, not a verb. A tombstone anywhere else dies immediately with the exact O-000 message. This mirrors the dissertation's rule that tombstones fire at the lexer: the fastest error the toolchain can produce.

Twins and their two sub-blocks are handled by a small state machine: seeing membrane { or attention { switches the parser into that block until the closing }; a bare } otherwise closes the twin. Everything else falls through the RX table in order (hold, seek, owe, decide, express, bond), and an unmatched line is a parse error. (assume role and stake are grammar-legal but v0.1-unparsed; see the pragmas.)

One semantic action happens at parse time: owe emits its structural status hold. owe review(atlas) to raj by fri also records hold status(atlas.review) = in-progress on the ower, because a commitment implies the counterparty's standing interest in its status. If you port nothing else faithfully, port this. The dinner mesh's third flow depends on it.

The engine, function by function

Six small functions, each one clause of the semantics:

• sel_match(selector, fact): membrane selectors as patterns. A bare ident gets (*) appended, * becomes a regex wildcard, and the match must cover the whole fact. This is what makes eta(*) and status(atlas.*) work.
• audience_match(sender, party, receiver): the circles pragma. all matches everyone; family and team match any receiver the sender bonds trust high; others matches everyone who is not; a name matches itself.
• membrane_cast(sender, fact, receiver): walks the sender's rules in declaration order and returns the first match. Returning None means no rule matched, and None means no flow: default-deny is a return value, not a policy option.
• cast_weight(tr): the M factor. exact 1.0, coarse(…) 0.7, category 0.5, existence 0.3, deny 0.0, and 0.0 for None.
• theta_for(receiver, sender): the receiver's bonds pick the sender's class (family if the receiver bonds the sender trust high, else others), then the receiver's own threshold declarations override the defaults family 0.3 / team 0.4 / others 0.8. Take note whose state is consulted here: the receiver's. Axiom III is a function signature here.
• pressure(...): the formula, with v0.1's constants visible. R is 1.0 (no semantic embedding yet), U is 1.3 if the gap has a deadline else 1.0, T comes from the receiver's trust table (high 1.0 / medium 0.6 / low 0.3), C is 0.0. The load-bearing line is exact:

    return R * U * T * M - C, (R, U, T, M)

• apply_cast(value, tr): v0.1's textual rendering of granularity casts. exact passes through, coarse yields ~value [coarse(30m)], category yields value [class-level], existence yields [exists].

settle()

The engine proper, in the order the trace prints:

Resolutions first. --resolve twin:fact=value arguments are applied before any flow: the named decide is deleted and the chosen value becomes a hold. Human judgment is an input type. The solver cannot choose a venue, not in v0.1 and not ever; that refusal is a permanent feature of the runtime contract.

The bound, announced. The engine records g0 = mesh.gapcount() and prints it with Theorem 1's promise: equilibrium in ≤ g0 flows.

The human lane delivers first, verbatim. Every express is appended to its recipient's lane and printed with its provenance label, before a single pressure calculation runs. Axiom V is not a special case inside the loop; it is a separate, earlier loop.

Then the loop. Each iteration scans all (receiver-gap, sender-hold) pairs. Note the direction: it iterates over receivers' gaps and looks for matching holdings, which is why unsolicited flow is unrepresentable rather than forbidden. For each pair it asks the membrane for a cast (skipping None and deny), computes P and the receiver's θ, and remembers the best P strictly above θ. If no candidate clears, the loop ends: equilibrium. Otherwise the best flow fires: the cast value is absorbed into the receiver's holds, the gap is popped, placement is ledger if the gap carried else escalate and silent otherwise. And then comes the confession:

        assert flows <= g0, "Theorem 1 violated — impossible"

The proof guarantees this assert can never trip. It ships anyway, in every habitat, so that an implementation that betrays the semantics confesses instantly instead of drifting quietly.

The report. Equilibrium is announced against the bound; the zero counters (messages composed by humans: 0, interruptions: 0) are printed because they are the product; ledgers list what surfaced; surviving gaps are listed as open (with a note when else sync will schedule live time); unresolved decides wait as "awaiting human judgment." And when nothing remains at all: open gaps: 0 — silence is a fixpoint.

Porting checklist

A new implementation may call itself Osmol v0.1 when it can look the reference in the eye:

1. Same trace text. Run dinner.osmol with the venue resolution; your output should match the reference byte for byte. That is the seed of the conformance suite, and differential testing against osmol.py is the cheapest oracle you will ever get.
2. Same constants. Trust weights, cast weights, default thetas, U = 1.3. All of them, exactly.
3. Same pragmas. Honor every documented simplification in the v0.1 pragmas, or supersede them consciously via RFC, never silently. (One known sharp edge: the dissertation's determinism rule mandates a lexicographic (sender, receiver, fact) tie-break among equal-pressure flows; the reference resolves ties by scan order. Implementing the mandated tie-break is standing RFC-shaped work.)
4. Same runtime assertion. Flows ≤ initial gapcount, asserted, in every habitat, forever.
5. Then graduate. When the single file feels small, the five-stage compiler of the engineering dissertation (Ch. 2), that is lexer, parser, semantic analysis, .odb lowering, and verification hooks, is the road from interpreter to toolchain, and one engine, four habitats is the destination.

The reference will eventually be the slow implementation. It will never be the wrong one. Its retirement job is being the oracle that certifies its successors.

The v0.1 Pragmas (Normative)

The header of osmol.py documents five deliberate simplifications, the v0.1 pragmas. They are not implementation trivia. For v0.1 they are normative: they define what the language actually does today, and every successor implementation must either honor each pragma or consciously supersede it through the RFC process. A successor that silently diverges from a pragma is not more correct than the reference interpreter; it is nonconforming.

This chapter promotes each pragma to its proper status: statement, rationale, required behavior, and how to test for it.

Pragma 1, Circles derive from bonds

Statement (from the header): a sender's membrane audience family/team matches any party the sender bonds with trust high; others is the rest.

Rationale. v0.1 has no social-graph model; the only relationship signal in the language is bond. Deriving audience classes from trust-high bonds gives membranes real semantics with zero new syntax.

Required behavior. When evaluating a membrane rule selector -> family: … or -> team: … in twin A against receiver B, the rule matches iff A declares bond b { trust high } for B. -> others matches iff A does not bond B trust-high. -> all matches everyone; a bare name matches that twin exactly. Separately, the receiver's class for a sender (which selects θ) derives from the receiver's own bonds: trust-high sender ⇒ family, otherwise others.

Test hint. Remove bond raj { trust high } from maya in dinner.osmol: the eta(*) -> family: exact rule stops matching, the -> others: coarse(30m) rule takes over, and raj's threshold class for maya flips to others.

Pragma 2, Wall-clock time is not simulated

Statement: deadlines raise urgency (U = 1.3) and drive escalation notes, but quiet hours are stored only.

Rationale. A clock in the settle loop would make traces depend on when you run them, and that is fatal for golden-file testing. So v0.1 collapses time to one bit: has a deadline, or not.

Required behavior. Any by clause on a gap sets U = 1.3; no deadline means U = 1.0. No gradual promotion, no lateness detection. quiet ranges parse and store but are never consulted. Sync-tagged gaps still open at equilibrium print the sync will be scheduled note rather than booking anything.

Test hint. Delete by 19:00 from raj's eta gap: the t2 flow's pressure drops from 1.30 to 1.00, and nothing else changes.

Pragma 3, owe auto-supplies status

Statement: owe X(args) auto-emits hold status(args.X) = in-progress on the ower.

Rationale. Spec §3: commitments generate structural gaps automatically; an unmet owe implies the counterparty's seek for its status. Structural demand needs structural supply, or the implied gap could never close.

Required behavior. Parsing owe review(atlas) to raj by fri in maya's twin emits hold status(atlas.review) = in-progress (argument path first, then the fact name), unless she already holds that fact explicitly.

Test hint. This is why t3 exists in the canonical trace: raj's seek status(atlas.review) drinks from a holding maya never wrote.

Pragma 4, decide requires human judgment

Statement: the engine cannot choose. Resolutions are injected via --resolve twin:fact=value.

Rationale. This one is different from the other four. It is no simplification at all but a permanent feature of the runtime contract (dissertation Chapter 3): human judgment is an input type, not a solver capability, in every habitat, always. No future implementation may supersede it.

Required behavior. An unresolved decide does not block settlement. The mesh settles around it: every other gap that can close will close, the engine declares equilibrium for what remains, and the open gap plus the waiting decide are reported in the footer as awaiting human judgment ... machines do not choose venues. We verified this against the interpreter: the dinner mesh without --resolve reaches equilibrium after 2 flows with the venue gap still open. A resolution must name one of the enumerated options, deletes the decide, and emits the corresponding hold.

Test hint. Run the dinner mesh without --resolve: maya's venue gap survives to the footer and raj's decide prints as awaiting judgment. See Resolving Decides.

Pragma 5, Placement

Statement: express → human lane (verbatim, delivered first); escalate-tagged gaps → ledger; everything else → silent. Interrupts exist but demand a passed escalate deadline, which needs wall-clock: unused.

Required behavior. The human lane delivers before any flow, untransformed, provenance-labeled. A delta absorbed into a gap declared else escalate appends to the receiver's ledger; all other deltas are silent. No flow ever places as interrupt in v0.1, and every trace footer truthfully prints interruptions: 0.

Test hint. The canonical trace's [ledger] on t1 and [silent] on t2/t3 are exactly this pragma.

The constant tables

These values are normative for v0.1; changing any of them is a semantics change and therefore edition-visible.

Not implemented in v0.1

Equally normative is knowing what the reference interpreter does not do:

• roledecl (assume/yield role): parses nowhere; semantic addressing waits for the mesh's role registry. See the wire roadmap.
• stake: unparsed; the anti-spam economics need a reputation ledger and, ultimately, Theorem 5.
• when conditions on membrane rules: parsed and stored, never evaluated. The Rust checker takes these up in osmol-core Stage 3.
• Number trust levels (trust 0.8): the grammar allows them; the engine knows only the three words.
• Lexicographic tie-break: the spec-level rule orders equal-pressure flows by (sender, receiver, fact); v0.1 uses iteration order, and the two visibly disagree even on the shipped corpus. In the canonical dinner trace, the equal-pressure t1/t2 flows fire in scan order, where the lexicographic rule would fire maya's eta before raj's venue (see the honesty note in the pressure chapter). The Rust solver must implement the real rule; reconciling the golden trace with it is an open, RFC-shaped decision.

Each absence is a rung on the build ladder, not a hole in the language. The pragmas are the honest boundary line between the two, and the reference interpreter's header is where that line is signed.

Conformance and Differential Testing

The suite is the language

Osmol's truth lives in three places, in constitutional priority order: the conformance suite, the specification, and only then any implementation, including the reference one. GOVERNANCE.md states the order plainly, and the engineering dissertation calls the first clause what it is: constitutional, amendable by nothing. The suite, not the reference implementation, is the arbiter.

The suite itself is a simple thing: a repository of golden .osmol programs, each paired with a required outcome. Two kinds of pair exist:

• Must-fail programs paired with expected diagnostics: code, span, and message class. spam.osmol must die with O-000 at line 2, in every implementation, forever.
• Must-run programs paired with expected deterministic settlement traces. Same declarations, same injected human judgments, same trace, byte for byte, on every platform.

Any implementation claiming the name Osmol must pass it. This is how the language stays bigger than its first codebase, and how Law VII (federated, or failed) grows teeth: a protocol whose behavior is defined by whichever binary you happen to run is not a protocol, it is a product with documentation.

The seeds

Honesty first: the conformance repository does not exist yet. What exists is its first two cases, which are already canon because they ship with the reference interpreter.

Seed 1, the dinner mesh (must-run). Input: dinner.osmol plus the canonical resolve command. Required output: this exact trace.

$ python3 -m osmol dinner.osmol --resolve "raj:venue(dinner)=verde"
OSMOL v0.1 - reference interpreter
parsed dinner.osmol: 2 twins, 0 sends (no such construct exists)
initial gapcount: 3   (Theorem 1 bound: equilibrium in <= 3 flows)
  [human judgment] raj resolves venue(dinner) = verde
  human-lane  maya -> raj  (verbatim, provenance=human): "Saw a fox on the way home and thought of you."
t1  raj.venue(dinner) --exact--> maya   P=1.30 (R1.0*U1.3*T1.0*M1.0) > theta[family]=0.3   [ledger]
t2  maya.eta(dinner) --exact--> raj   P=1.30 (R1.0*U1.3*T1.0*M1.0) > theta[family]=0.3   [silent]
t3  maya.status(atlas.review) --category--> raj   P=0.65 (R1.0*U1.3*T1.0*M0.5) > theta[family]=0.3   [silent]

EQUILIBRIUM after 3 flows (Theorem 1 bound 3: respected)
messages composed by humans: 0 (the grammar has no verb for it)
interruptions: 0
ledger[maya]: venue(dinner) = verde
open gaps: 0 — silence is a fixpoint

Seed 2, the spammer (must-fail). Input: spam.osmol. Required outcome: O-000 at line 2.

$ python3 -m osmol spam.osmol
OSMOL v0.1 - reference interpreter
osmol: line 2: error[O-000]: 'send' — there is no send. Declare what you hold; declare what you seek; the mesh does the rest.

Two cases sounds thin. But look at what they already pin down between them: the tombstone lexer, one full parse of every major construct, the resolve pathway, the human lane's verbatim-first delivery, membrane casts at two granularities, the pressure arithmetic and threshold classes, placement (ledger vs silent), and the Theorem 1 bound. The dissertation's build order makes every subsequent step's definition of done a conformance addition, so the suite grows as the ladder climbs.

Differential testing

The plan for the Rust engine (see One Engine, Four Habitats) does not retire the Python interpreter, it re-employs it. During the transition both engines run identical corpora and their traces are diffed byte-for-byte. The Python interpreter's retirement gift is becoming the oracle that certifies its successor: Step 1 of the build order is done when osmol check matches Python's judgments on the corpus, and Step 2 is done when the settlement traces are byte-identical.

The precondition for any of this is determinism, which is why the tie-break rule is spec-level: among fireable flows of equal pressure, order lexicographically by (sender name, receiver name, fact). Without a fixed tie-break, two correct engines could settle the same mesh along different orders and both be "right", and then golden-file testing, membrane audits, and cross-implementation trust would all dissolve. Determinism is what makes a trace a fact about a program instead of an anecdote about a run.

One honest wrinkle, already documented in the pressure chapter: Seed 1's golden trace comes from the Python engine, whose tie-break is scan order, and on the dinner mesh that order differs from the mandated lexicographic rule (t1 and t2 tie at 1.30 and fire in the "wrong" order). Before Step 2's byte-identical goal can be met, the project must either re-derive the golden trace under the lexicographic rule or supersede the rule by RFC. The suite cannot canonize both.

The adversarial layer

Beneath the golden files sits the layer that goes looking for trouble:

• Property tests (proptest) generate random meshes and assert the machine-checked invariants dynamically: flows never exceed the initial gapcount (Theorem 1's runtime shadow), denied membranes leak nothing, and granularity never refines along any path. The theorems say these cannot fail; the property tests are how an implementation proves it read the theorems.
• Fuzzing (cargo-fuzz) hammers the lexer and parser, because parsers are where languages get owned.
• The CI matrix builds what the doctrine demands: native Linux, macOS, and Windows; wasm32-unknown-unknown; and the Android FFI target, all against the same suite. Divergence between habitats is, by definition, a bug in whichever habitat disagrees with the suite.

Contributing a case

A conformance case should eventually be a small, self-describing bundle. One suggested shape:

cases/
  o-000-spam/
    input.osmol          -- the program
    cmd.txt              -- exact invocation, including any --resolve flags
    expected.txt         -- golden trace, or expected diagnostic (code, span, class)

New cases that pin down existing spec behavior are ordinary pull requests. Cases that would change what the language means are language changes, and those go through the RFC process. Remember the authority order: a merged suite case outranks everything, so merging one is the most consequential act in the project.

One last honesty clause, from the dissertation's risk chapter: the gravest failure mode for a young language is the one-implementation trap, where the reference quietly becomes the spec and every accident of its code hardens into law. The suite's constitutional supremacy is half of the counter; the other half is keeping the Python engine alive as a second implementation long after it stops being the fast one. Two engines, one suite, byte-identical traces: two vessels, one level.

The Wire Ahead: .odb and OMP

None of what follows is implemented. There is no network transport today. Not duo mode, not the edge, not the SMTP gateway, not one byte of OMP. The v0.1 interpreter settles all twins inside a single process, and that is the entire running surface of the language. This chapter documents the specified road, from the engineering dissertation, so that implementers aim at the same wire. Expect RFCs before code; where this chapter and a future accepted RFC disagree, the RFC wins.

The language and the wire are separate standards, the same way HTML and HTTP are separate standards. Osmol says what a twin is; the Osmol Mesh Protocol (OMP) says what crosses between membranes. Keeping them separate is what lets either evolve without breaking the other, and it also keeps the protocol bigger than any one implementation.

The .odb

Osmol source never deploys. The compiler's lowering stage (dissertation Ch. 2, stage 4) emits the three deployment artifacts of spec §6, that is a typed state schema, a membrane policy set, and gradient triggers, and serializes them together as the Osmol Deployment Bundle (.odb): canonical CBOR, content-hashed, and signed. The .odb is what actually travels to a membrane object.

The properties are the point. Canonical CBOR means the same twin lowers to the same bytes everywhere, so bundles can be compared, cached, and audited. Content-hashed means a membrane can verify it is running exactly the policy its owner compiled. Signed means it can prove who compiled it. And source never deploys means the mesh side needs no parser, no compiler, and no opinion about surface syntax. An edge membrane consumes lowered artifacts only, which keeps the trusted surface small.

OMP

OMP's atom is the delta envelope: canonical CBOR carrying subject, predicate, value, granularity coordinate, validity window, provenance chain, authorship class, a nonce, and a detached signature over all of it. Deltas are content-addressed by their hash, which gives replay detection and audit logs for free: a membrane that has seen a hash before drops the duplicate, and an append-only log of hashes is a verifiable history.

Transport is deliberately boring: WebSocket or HTTP/2 between membranes, because boring transports are how protocols survive. Protocol version is negotiated as omp/0, with frozen semantics per version, the same discipline as editions on the language side.

Everything on the wire is deltas, except exactly four control message types:

1. Gap advertisements: how a membrane lets linked membranes know what its twin seeks, so pressure can be computed at all.
2. Role-registry queries: resolution of @role(...) parties at flow time; the missing half of semantic addressing.
3. Stake attachments: the reputation escrow that makes stake real between strangers.
4. Sync-escalation handshakes: how two membranes jointly book live human time when an else sync gap survives its deadline.

That the list is short, closed, and enumerated is a design commitment: a wire whose control plane grows freely becomes a second application layer, and then a second inbox.

The legacy adapter

The SMTP gateway is specified as part of OMP, not bolted on. Inbound, it decomposes conventional mail into candidate assertions and gaps tagged provenance: unverified-legacy, which then enter the ordinary pipeline as external pressure. Your inbox, a technology from already 1971, equalized into your twin. Outbound, it serializes a delta as a well-formed email for counterparties still living in 1971.

This is the adoption physics of the whole project (Osmosis spec §11; the Fifty-Year Letter's museum chapter). A communication tool is worth nothing until the other person has it. This cold-start problem is what killed Google Wave. The adapter makes Osmol pay for itself single-player, on day one: an ambassador that triages your existing email is valuable even if no one else on Earth adopts anything, and the native protocol grows underneath it, sender by sender. Disruption by absorption, not by siege. Treating the gateway as a first-class protocol component, with its own conformance surface, is what keeps that promise honest.

The crypto layer

Dissertation Ch. 5, compressed. Each participant's identity is an Ed25519 keypair generated and held in platform secure hardware (Android Keystore with StrongBox where available, Secure Enclave on iOS), with signing performed on-silicon, so the private key is never process memory. Every delta is signed over payload ‖ provenance chain ‖ authorship class ‖ nonce, which makes the authorship label (human / assisted / autonomous) a cryptographic claim rather than metadata: forging "a human wrote this" means forging a signature. This is Axiom V made of silicon, the enforcement story behind O-005.

Key rotation is a signed succession chain. Revocation is a tombstone delta, the one place that word is permitted, as a noun. The envelope carries a versioned sig-alg field from day one, because the only unforgivable crypto decision is the unversioned one. And the endgame moves membrane evaluation into attested TEEs, so that the mesh operator is technically incapable of reading state. Portability plus blindness, that combination is what keeps the filter layer from becoming anyone's cage.

Where an implementer plugs in

The first wire milestone is duo mode (dissertation Ch. 3, and step 4 of the Ch. 11 build order): two osmold daemons, one per twin, on one machine or LAN, membranes speaking OMP over localhost. It is the smallest deployment in which a membrane crossing is real (two processes, two policies, one wire), and it is where every OMP design question first meets running code. Edge mode follows (step 5: one Durable Object per twin consuming .odb deploys, with the append-only audit log), then device mode (step 6: the core linked into a phone with hardware-held keys).

If you are implementing Osmol in another language, the sequencing advice is the dissertation's: get your engine byte-identical with the conformance suite in local mode first. The wire multiplies whatever semantics you already have, including the wrong ones. If you want to shape the wire itself, the road runs through the RFC process: omp/0 will be frozen the day it ships, so the time to argue about the envelope is now, while it is still paper.

There is no send. And soon there will be no send over a network, which is harder and better.

Governance and Licensing

Osmol installed its governance at population one, before it had a second contributor, let alone a second user. That was deliberate. The engineering dissertation states the reason plainly: governance retrofitted after adoption is how open protocols quietly become products. This page documents what the governance file actually says, and what the license actually permits.

The source of truth is GOVERNANCE.md in the osmol-lang/rfcs repository. Everything below is a faithful rendering of it; where the two ever differ, the file wins.

Who decides

Osmol currently has one maintainer, its founding keeper, named and signed in GOVERNANCE.md. The maintainer may appoint co-maintainers at any time by amending the file. This is the ordinary shape for a young language (a benevolent dictator, explicitly temporary). What is unusual is only that it is written down, versioned, and bound by the clauses below from day one.

What defines the language

In order of authority, quoting the file:

1. The conformance suite (when it exists): programs and their required outcomes.
2. The specification at osmol-lang/spec.
3. The reference implementation, "which serves the two above and never overrules them."

Note what is not on the list: the maintainer's opinion of the moment, and any particular codebase's convenient behavior. When the suite exists, an implementation is Osmol if and only if it passes, the reference one included. See Conformance for how the suite grows.

The constitutional clauses

Two clauses in GOVERNANCE.md are marked amendable by nothing. Verbatim:

1. Osmol's specification, suite, and reference code remain under irrevocable open licenses.
2. Conforming implementations must honor the portability guarantee: a participant's membranes, models, and logs export and rehost losslessly.

The first clause keeps Osmol a protocol rather than a product: no future steward, including the founding one, can take the language private.

The second one deserves some attention, because it is a conformance requirement, not a courtesy. A participant's membrane is the most sensitive filter ever attached to a life; whoever hosts it curates that person's reality. The Fifty-Year Letter names this the gravest risk of the whole design: a filter you do not control is a cage with good UX. The portability guarantee is the structural answer (dissertation, Chapter 10): if your membranes, models, and logs export and rehost losslessly on any conforming mesh, then no host, the project's own infrastructure included, can convert the filter layer into a captive position. An implementation that stores state in a roach motel is not a lesser Osmol; it is not Osmol at all.

The dead-man clause

GOVERNANCE.md closes with succession, the outlive-me clause, verbatim:

If every maintainer is publicly unreachable for 12 consecutive months, stewardship passes to the most spec-conformant actively maintained public fork, which may claim continuity of the Osmol name. The stone belongs to whoever keeps carving it faithfully.

Note the tie-breaker: not the loudest fork, not the biggest, but the most spec-conformant one. Even succession is decided by the authority list above.

Licensing

Everything is MIT, everywhere (spec, reference interpreter, proofs, this book), under the copyright line:

Copyright 2026 The Osmol Language Contributors

For an implementer, MIT means exactly what you hope: build Osmol in any language, embed it in anything, commercial use is fine, forking is fine. Keep the copyright notice and license text in your distribution, and you owe nothing else. There is no CLA, no patent gate in the license, no "open core" seam waiting to close.

One planned refinement: the specification may later add CC-BY or Apache-2.0 as parallel license options, add-only, never subtract. A document already released under an irrevocable license stays released; future versions can only widen the grant. This is the licensing face of the first constitutional clause.

How change happens

Grammar and semantics changes ship only in editions, and enter through the RFC process: a pull request to osmol-lang/rfcs describing the change, its motivation, and its effect on the spec and suite, accepted or declined by maintainers with written reasons. Lightweight at today's population, and installed anyway, for the reason this page opened with.

Related

• The RFC Process: how to propose a change
• Versioning and Editions: how change ships without breaking a deployed mesh
• Conformance: the suite that sits at the top of the authority list

The RFC Process

How the language changes

Osmol changes in public, on the record, or not at all. Anyone may propose a change by opening an RFC: a pull request to the osmol-lang/rfcs repository describing the change, its motivation, and its effect on the spec and conformance suite. Maintainers accept or decline with written reasons, so a declined RFC leaves behind an argument, not a silence. Also, grammar or semantics changes ship only in editions: accepted language changes wait for the next coherent snapshot rather than trickling into a moving target, so a deployed mesh never breaks under anyone's good idea.

The process is deliberately lightweight. In the engineering dissertation's words, it is "lightweight at population two, but installed now, because governance retrofitted after adoption is how open protocols quietly become products." The full constitution, including the two clauses no RFC can amend (irrevocable open licenses; lossless portability of membranes, models, and logs), lives in Governance and Licensing.

The template, walked

Every RFC starts from 0000-template.md, five sections long:

• Summary: one paragraph on what changes. If you cannot say it in a paragraph, the RFC is not ready.
• Motivation: why the language needs this, and (the template's own requirement) "Which of the five axioms it serves." An RFC that serves no axiom is probably a feature for a different language.
• Design: the change stated precisely, with grammar diffs against the EBNF, semantics, and diagnostics. If your change deserves a new error, name its O-code and write its message; in this language the errors are the ethics.
• Effect on spec and conformance suite: which spec sections change, and which new test programs must exist. This section has teeth: the conformance suite defines the language, so a change that adds no golden program has not really been specified.
• Drawbacks and alternatives: what this costs, and what else was considered. An RFC that cannot argue against itself is a brochure.

What makes a good RFC

Practical guidance, all of it derived from canon:

• Cite the axiom. Not as decoration: show which of the five axioms your change strengthens, and check that it weakens none.
• Bring the golden test case. Arrive with the .osmol program and its expected trace or diagnostic. A change you can express as a golden file is a change two implementations can agree about.
• Respect the constitutional clauses. Nothing that closes a license; nothing that traps a membrane, model, or log.
• Supersede pragmas explicitly. The v0.1 interpreter's documented simplifications are normative until replaced. An RFC that says "the circles pragma is retired; audience classes now resolve like this" is a gift; an implementation that silently diverges is a bug with a personality.

RFC-shaped work already waiting

This book has been quietly leaving invitations in its margins. Collected:

• Theorems 2-5 formalizations: enrich the Theorem 1 oracle back into structure; see the open theorems.
• Retraction semantics: un-asserting a hold that has already equalized needs revocation-deltas; spec §10 defers it to you.
• Gap privacy: seeking is itself revealing; membranes should govern the visibility of gaps, not only holdings.
• Lattice registry entries: standard grains per domain; see the granularity lattice.
• The lexicographic tie-break: mandated by the determinism rule, unimplemented in the reference; see the interpreter walkthrough.
• role and stake implementation: two constructs the grammar promises and v0.1 does not yet parse; see roles and stake.

Pick one, open the pull request, and argue it well. The stone belongs to whoever keeps carving it faithfully.

Versioning and Editions

Osmol separates two questions that projects often blur: how tools are numbered, and how the language changes. Tools follow semver. The language follows editions. Keeping them apart is what lets the toolchain move fast while a deployed mesh never breaks.

Tools follow semver

Binaries, interpreters, and libraries version like any software (dissertation Chapter 10). The current reality is uniform: v0.1.0 everywhere. The spec release (tagged "the first stone"), the osmol repository release, and the osmol package on PyPI all carry the same number. As the Rust crates arrive (osmol-core, osmol-cli, osmol-wasm, osmol-ffi), each will walk its own semver path; a patch release of a tool promises no change to language behavior at all.

The language follows editions

An edition, Rust-style, is a coherent grammar-and-semantics snapshot. Edition 2026 is this spec. The mechanism that makes editions safe in a communication language is distinctive: membranes advertise the editions they accept, letting the language evolve without ever breaking a deployed mesh. Your twin can adopt edition 2027 while your grandmother's membrane keeps speaking 2026, and the mesh negotiates between them, the same way OMP freezes semantics per protocol version (omp/0, dissertation Chapter 4). Nothing about upgrading a language is allowed to feel like being cut off.

Docs version with the language

The documentation site pins to editions too (dissertation Chapter 9): /v0.1/ freezes the day /v0.2/ opens, so a program written against an old edition never loses its reference. This book carries its edition on the cover; when you cite it, cite the edition.

What forces an edition

Only grammar or semantics changes, and they enter exclusively through the RFC process. The boundary is wider than it looks at first:

• Pragma supersessions count. The v0.1 pragmas are normative; consciously replacing one (say, simulating wall-clock time so quiet becomes enforced) changes what programs do, and is edition territory.
• Constants count. The trust, cast, and threshold tables are semantics; a mesh where category weighs 0.6 settles differently than one where it weighs 0.5.
• Diagnostics wording counts. The errors are the ethics, so the O-xxx messages are normative text; changing one is edition-visible, not copyediting.

What does not force an edition: new tooling, new habitats, performance work, documentation, in short anything that leaves every conforming program's trace byte-identical.

The stability promise to implementers

The conformance suite tags every test with the edition it belongs to, and an implementation states which edition it targets. That single sentence, "targets edition 2026", is the whole compatibility contract: pass the suite for your edition and you may call yourself Osmol; the suite, not any implementation, is the arbiter (see Governance and Licensing). Editions are how the language gets to grow for fifty years without ever asking a settled mesh to move. The stone doesn't rush.