The two fixpoints, made one construct.

μ and ν are dual operators on monotone functors.

In conventional languages, μ is privileged — you write data, and ν is hacked on (a loop, a thread, a generator). Each fights a different battle with the runtime.

In Munu, both are first-class. A contract is the term-level witness that an algebra (μF → A) and a coalgebra (B → νG) agree on a boundary. The kernel never sees this; it sees only bytecode that steps when bound.

Contracts all the way down.

Every contract runs on its own lightweight thread in the kernel. A contract binds mu functions (what you build) and nu functions (what you observe) under a supervised behaviour. The do: clause governs local failure recovery. The must: clause is the obligation the supervisor enforces. When a thread crashes, it crashes only that contract — the supervisor decides whether to absorb the failure and deliver a degraded result, restart, or escalate.

When an LLM's generated code crashes at runtime, the supervisor catches the thread failure, formats a structured diagnostic, and feeds it back through the same dataflow variable the caller is waiting on. The LLM sees what went wrong, fixes the code, and retries — without losing context. The harness turns a thread crash into a conversation.

// timing envelope: 95% within 100ms, 99% within 500ms
cdf fast_response = [(100ms, 0.95), (500ms, 0.99)]

mu nand(a: bool, b: bool) -> bool {
    (true, true) => false,
    (_, _) => true
}

nu nand_combine(a_s: [bool], b_s: [bool]) -> [bool] {
    ([a | at], [b | bt]) =>
        [nand(a, b) | nand_combine(at, bt)]
}

pub contract NandGate(a: [bool], b: [bool]) -> [bool]
    behaviour {
        do:
            nu X.
                [fail(self, _)] <restart(self)> X
                and [_] X
        must:
            nu Y.
                [fail(self, _)]~fast_response
                    <restart(self)> Y
    } {
    spawn nand_combine(a, b)
}

// contracts compose contracts
pub contract AndGate(a: [bool], b: [bool]) -> [bool] {
    let nand_out = spawn NandGate(a, b);
    spawn NandGate(nand_out, nand_out)
}

Every variable is a dataflow variable.

Every variable in the kernel has a 6-state lifecycle. Variables are single-assignment — once Bound, they never change. Reads block until the value arrives. There are two paths through the FSM: eager variables that are allocated unbound and computed immediately, and lazy variables whose producer parks until a consumer demands the value.

Failure states: When a contract's do: fires Restart, its unbound variables go TempFail — recoverable when the producer restarts and binds. When a child breaches its must: or the supervisor escalates, variables go PermFail — terminal, no recovery.

Eager dataflow: Unbound → Needed → Bound

When a contract calls a nu function or another contract, the callee runs on its own thread. The result variable starts Unbound. If the caller reads it before the callee finishes, the caller's thread suspends until the value is bound.

nu produce(n: i64) -> [i64] {
  n => [n * 2 | produce(n + 1)]
}

mu head_of(xs: [i64]) -> i64 {
  ([h | _]) => h
}

pub contract Eager(n: i64) -> [i64] {
  let stream = spawn produce(n);  // spawns produce on its own thread
  spawn head_of(stream)           // blocks until first element is Bound
}

Lazy dataflow: WaitNeeded → Needed → Bound

A lazy mu function returns immediately with a WaitNeeded variable — the body doesn't execute. When something demands the result (arithmetic, match, or a read), the body wakes and runs.

// body does not run until result is demanded
lazy mu compute(n: i64) -> i64 {
  (n) => n * 2
}

mu use_result(n: i64) -> i64 {
  (n) => {
    let result = compute(n);  // returns WaitNeeded — body does not run
    result + 5              // demands result → body wakes, returns 25
  }
}

pub contract Lazy(n: i64) -> [i64] {
  spawn use_result(n)
}

A ψ-term lattice with a 6-state FSM.

Gradual typing without an escape hatch. The checker proceeds by subsumption (⊑), never equality. GLB is ν (greatest fixpoint); LUB is μ (least fixpoint). The μ–ν duality at term level repeats at type level — same operators, same lattice.

Errors written for the LLMs, not the human.

The compiler is the first reader; the LLMs are the second; the human, when they choose to look, is the third. Every diagnostic emits a structured envelope with the failing constraint, the relevant positions in the AST, a candidate-fix vector, and the smallest counter-example that violates subsumption.

This is the language-level invariant that makes Munu an AI harness: the models never have to guess what the compiler meant — the constraint and a witness for its violation are both addressable terms.

error[E0308]: mismatched types
  --> src/main.uv:14:18
   |
14 |     let n: u64 = raw
   |                  ^^^ expected u64, found ψ
   |
   = help: add a cast

{
  "code":       "M.subsume.fail",
  "operator":   "⊑",
  "expected":   "u64",
  "got":        "ψ",
  "site":       "src/main.uv:14:18..14:21",
  "constraint": "ψ ⊑ u64",
  "witness":    { "raw": "-3.14" },
  "fixes": [
    { "k": "insert_cast",  "term": "raw as u64" },
    { "k": "widen_target", "term": "i64" }
  ]
}