Learn / Worked Examples

Worked Examples

Section: LearnLast updated: 2026-02-11

How to Read These Examples

These examples are not meant to show every feature of .matr. They are meant to do something more important:

  • make the platform understandable
  • demonstrate that the execution loop is concrete
  • show what “verifiable” looks like If you can follow these examples, you can reason about the rest of the documentation.

Example 1 — Logic Primitive: Bounded AND

Goal

Define a simple logical operation as a material program:

  • two boolean inputs
  • one boolean output
  • an observable output signal This is intentionally basic. It’s the “hello world” of deterministic behavior.

.matr intent

module examples.logic.and
version 1.0.0
type Bit = enum { 0, 1 }
intent and_gate(a: Bit, b: Bit) {
  // Output is observable and bounded.
  emit signal OUT = (a == 1 && b == 1) ? 1 : 0
}
profile simulation.strict

What the compiler enforces

  • Inputs are typed (Bit) and closed (only 0 or 1)
  • Output is explicitly declared as an observable signal
  • The intent is finite and bounded

What the artifact (Molebyte) carries

At a public level, the compiled artifact contains:

  • the input declarations
  • the output declaration
  • the transition structure (in this case, direct evaluation)
  • identity (hash) and version lineage

What a run binds

A run binds:

  • the Molebyte artifact (the compiled and_gate)
  • the simulation.strict profile
  • a policy (e.g., strict pass/fail on any mismatch)
  • input values, such as (a=1, b=0)

Expected signals

Given inputs:

  • (0,0) → OUT=0
  • (0,1) → OUT=0
  • (1,0) → OUT=0
  • (1,1) → OUT=1 Forma records OUT as a typed signal.

What a diff might look like

If the observed OUT differs from expected OUT, the diff record classifies:

  • value mismatch If OUT is missing, the diff classifies:
  • missing signal

What judgment means

With strict policy:

  • any mismatch → FAIL
  • all matches → PASS The judgment is recorded with provenance.

Example 2 — Memory Element: Simple 1-Bit Latch

Goal

Show that .matr can describe a bounded memory behavior:

  • a write input
  • a stored state
  • a read output This example is intentionally minimal. It’s not claiming physical implementation details. It’s demonstrating that the control plane can model state.

.matr intent

module examples.memory.latch
version 1.0.0
type Bit = enum { 0, 1 }
type Mode = enum { IDLE, WRITE, READ }
intent latch(mode: Mode, din: Bit) {
  state stored: Bit = 0
  // A bounded state transition model.
  when mode == WRITE {
    stored = din
  }
  when mode == READ {
    emit signal Q = stored
  }
}
profile simulation.strict

What the compiler enforces

  • State (stored) is explicitly declared and typed
  • State transitions are finite and explicit
  • Outputs are observable and typed
  • No unbounded iteration exists

What a run looks like

To validate memory behavior, you don’t just run once. You run a short sequence under a profile that allows ordered steps. Example sequence:

  1. mode=WRITE, din=1
  2. mode=READ Expected signal:
  • Q=1 A second sequence:
  1. mode=WRITE, din=0
  2. mode=READ Expected signal:
  • Q=0 This is how state becomes verifiable.

What diffs mean here

If Q appears but is wrong:

  • value mismatch If Q never appears:
  • missing signal If the state violates declared bounds (it shouldn’t, because Bit is closed):
  • boundary violation

Why this matters

This example demonstrates that:

  • artifacts can carry state
  • state transitions can be bounded
  • outputs can reflect stored state That is the foundation for memory architectures.

Example 3 — Composition + Sweep

Goal

Show how a more realistic validation occurs:

  • two intents composed
  • a parameter sweep used to check envelope stability We’ll use:
  1. a threshold check
  2. a stabilizer that only emits if threshold holds

.matr intent

module examples.composed.stability
version 1.0.0
type Reading = float range [0.0, 100.0]
constraint safe_window(x: Reading) {
  x >= 40.0
  x <= 60.0
}
intent threshold(x: Reading) {
  require safe_window(x)
  emit signal OK = 1
}
intent stabilize(x: Reading) {
  require safe_window(x)
  emit signal STABLE = 1
}
profile simulation.tolerant

Composition

Composition here means:

  • both intents share the same constraint
  • both emit signals when valid In a realistic system, composition may involve chained signals. Publicly, the point is simple: You can validate composed behavior under one profile.

Sweep

A sweep tests across a range:

  • x from 0 to 100 Expected behavior:
  • for x in [40,60], OK=1 and STABLE=1
  • outside that range, constraint violation is recorded This creates a boundary map:
  • where behavior is valid
  • where it fails Sweeps are how you establish envelopes.

What the outputs look like

A sweep run produces:

  • signals per input value
  • a diff map (where constraints failed)
  • a summary of pass/fail across the range This is what makes a program feel like infrastructure. Not “it worked once.” “It behaves within declared bounds.”

What These Examples Prove (And What They Don’t)

They prove:

  • .matr expresses bounded intent
  • compilation produces stable artifacts
  • runs produce signals
  • diffs are structured
  • judgment is explicit They do not prove:
  • physical substrate mapping
  • sequence-level implementation
  • facility-scale execution That evidence belongs in Research. Learn’s job is to make the contract understandable.