A Complete Spine Program Explained

Post 15 · Phase 3 — Synthesis

Over the past fourteen posts, we have introduced Spine's concepts one at a time: facts, rules, effects, invariants, time, probability, processes, spatial structure, resources, universes, verification, and compilation.

This post brings everything together in a single program.

We will build a governed asset system — a system where agents own assets, transfers are governed by rules, permissions depend on context, and the entire structure is verified and compiled. It is small enough to read in one sitting, but rich enough to exercise every major feature of the language.

The Domain

Our system tracks three kinds of entities:

Agents — people, organizations, or automated systems that can own things and perform actions.
Assets — anything that can be owned, transferred, or composed into larger wholes.
Capabilities — permissions that govern what actions an agent may take.

Assets can be parts of other assets. Ownership can be transferred. Transfers require authorization. And the rules depend on where the system operates — a jurisdiction, an organization, a physical location.

Step 1: Structural Facts

We begin by declaring what exists and how things relate.

# Entity Types
Agent is an EntityType.
Asset is an EntityType.
Capability is an EntityType.

# Agents
Alice is an Agent.
Bob is an Agent.
TrustCorp is an Agent.

# Assets
Car is an Asset.
Engine is an Asset.
Wheel_FL is an Asset.
Wheel_FR is an Asset.

# Capabilities
CanTransfer is a Capability.
CanCompose is a Capability.
CanApprove is a Capability.

# Structural Facts
Engine is part of Car.
Wheel_FL is part of Car.
Wheel_FR is part of Car.

Alice owns Car.
Alice has capability CanTransfer.
Alice has capability CanCompose.
Bob has capability CanTransfer.
TrustCorp has capability CanApprove.

Car is identified by ASSET-CAR-001.
Engine is identified by ASSET-ENG-001.

These declarations establish the vocabulary of the system. They say what kinds of things exist and what relationships are possible — nothing more. No behavior, no constraints, just structure.

This is the fact-oriented foundation from the beginning of the series: we describe what is before we describe what happens.

Step 2: Constraints

Structure alone is too permissive. We add constraints — rules that the system must always satisfy.

it is obligatory that each Asset has at most 1 owner.
it is obligatory that the part-of relation is acyclic.
it is forbidden that an Agent transfers an Asset it does not own.

These constraints are not runtime checks. They are part of the system's logical definition. The compiler proves they hold — or rejects the program.

Step 3: Effects

Now we add behavior. Effects describe what can happen — actions with preconditions and postconditions.

TransferOwnership emits OwnershipChange.
TransferOwnership requires that the from_agent owns the asset.
TransferOwnership requires that the from_agent has capability CanTransfer.
TransferOwnership ensures that the to_agent owns the asset.
TransferOwnership ensures that the from_agent no longer owns the asset.

ComposeAsset emits CompositionChange.
ComposeAsset requires that the agent owns the parent asset.
ComposeAsset requires that the agent owns the child asset.
ComposeAsset requires that the child asset is not part of any other asset.
ComposeAsset ensures that the child asset is part of the parent asset.

Effects are not functions that execute imperatively. They are structured descriptions of state transitions. The preconditions and postconditions are part of the definition — they determine when the effect can fire and what the world looks like afterward.

Step 4: Resource Tracking

Some facts in this system should not be duplicated or discarded silently. Ownership is a prime example: if an agent owns an asset, that fact is consumed when ownership transfers. It cannot be copied.

Owns is a linear fact.
HasCapability is an unrestricted fact.

This is Quantitative Type Theory at work. The compiler tracks how many times each fact is used. A linear fact must be consumed exactly once — you cannot accidentally duplicate ownership or forget to account for a transfer.

Step 5: Processes

The system is not a single thread of execution. Multiple agents act concurrently, and their actions may need to be coordinated.

TransferRequested leads to TransferApproved.
TransferApproved leads to TransferCompleted.
TransferRequested leads to TransferRejected.

TransferApproval has probability 0.95.
TransferTimeout has probability 0.02.

AssetTransferProtocol guarantees that
  TransferRequested leads to TransferCompleted.
under fair scheduling of approvals, it is guaranteed that
  TransferRequested leads to TransferApproved.

These describe the temporal ordering of events, their probabilities, and the behavioral guarantees the system must satisfy. Under fair scheduling, every transfer request eventually reaches approval. The compiler can check these properties against the temporal model.

Step 6: Spatial Structure

Assets exist somewhere. An asset in a warehouse is different from the same asset in transit. The system tracks containment and locality.

Warehouse is a Location.
TransitZone is a Location.
Office is a Location.

Warehouse is located in Amsterdam.
Office is located in Amsterdam.
Amsterdam is located in Netherlands.

Car is located in Warehouse.

it is obligatory that a transfer requires both agents in the same location,
  or the asset in a TransitZone.

Spatial structure is not metadata attached after the fact. It is part of the system's definition, and constraints can reference it directly. The compiler verifies spatial invariants — an asset cannot be in two places at once, and containment hierarchies remain consistent.

Step 7: Universes

The rules so far have been universal. But in practice, ownership rules differ by jurisdiction, and organizational policies add further constraints.

within jurisdiction NL, it is obligatory that
  asset transfers above 10000 EUR require notarial approval
  [BW Art. 3:89].

within jurisdiction NL, it is obligatory that
  vehicle transfers are registered with the RDW
  [Wegenverkeerswet Art. 36].

within jurisdiction EU, it is obligatory that
  cross-border asset transfers are documented for customs
  [EU Regulation 952/2013].

Universes layer context onto the system. The base facts and effects are defined once in the General universe. Jurisdictions add regulatory constraints. Organizations add policy. A program compiled for one universe inherits and specializes the rules of its parents.

Step 8: Verification

Before compilation, the system is verified. The compiler produces verification artifacts for external tools.

verify constraint SingleOwner via z3.
verify temporal AssetTransferProtocol via tla+.
verify process TransferOwnership via mcrl2.

This is the proof pipeline. Each verification target extracts a different aspect of the same program: Z3 checks logical constraints (end-to-end working), TLA+ checks temporal properties (artifact generation), mCRL2 checks process behavior (artifact generation). Support for BigraphER (spatial invariants) and PRISM (probabilistic bounds) is planned.

Step 9: The Complete Program

Here is the entire governed asset system, assembled from the pieces above.

# Governed Asset System
# A complete Spine program demonstrating facts, rules, effects,
# constraints, spatial structure, temporal guarantees, and verification.

# === Entity Types ===
Agent is an EntityType.
Asset is an EntityType.
Capability is an EntityType.

# === Agents ===
Alice is an Agent.
Bob is an Agent.
TrustCorp is an Agent.

# === Assets ===
Car is an Asset.
Engine is an Asset.
Wheel_FL is an Asset.
Wheel_FR is an Asset.

# === Capabilities ===
CanTransfer is a Capability.
CanCompose is a Capability.
CanApprove is a Capability.

# === Structural Facts ===
Engine is part of Car.
Wheel_FL is part of Car.
Wheel_FR is part of Car.

Alice owns Car.
Alice has capability CanTransfer.
Alice has capability CanCompose.
Bob has capability CanTransfer.
TrustCorp has capability CanApprove.

Car is identified by ASSET-CAR-001.
Engine is identified by ASSET-ENG-001.

# === Constraints ===
it is obligatory that each Asset has at most 1 owner.
it is obligatory that the part-of relation is acyclic.
it is forbidden that an Agent transfers an Asset it does not own.

# === Spatial Structure ===
Warehouse is a Location.
TransitZone is a Location.
Office is a Location.

Warehouse is located in Amsterdam.
Office is located in Amsterdam.
Amsterdam is located in Netherlands.

Car is located in Warehouse.

it is obligatory that a transfer requires both agents in the same location,
  or the asset in a TransitZone.

# === Temporal Structure ===
TransferRequested leads to TransferApproved.
TransferApproved leads to TransferCompleted.
TransferRequested leads to TransferRejected.

# === Effects ===
TransferOwnership emits OwnershipChange.
TransferOwnership requires that the from_agent owns the asset.
TransferOwnership requires that the from_agent has capability CanTransfer.
TransferOwnership ensures that the to_agent owns the asset.
TransferOwnership ensures that the from_agent no longer owns the asset.

ComposeAsset emits CompositionChange.
ComposeAsset requires that the agent owns the parent asset.
ComposeAsset requires that the agent owns the child asset.
ComposeAsset requires that the child asset is not part of any other asset.
ComposeAsset ensures that the child asset is part of the parent asset.

# === Probabilities ===
TransferApproval has probability 0.95.
TransferTimeout has probability 0.02.

# === Value Types ===
AssetCode refines TextDomain by matching asset_code_pattern.
PositiveValue refines DecimalDomain by satisfying greater_than_zero.

# === Resource Tracking ===
Owns is a linear fact.
HasCapability is an unrestricted fact.

# === Behavioral Guarantees ===
AssetTransferProtocol guarantees that
  TransferRequested leads to TransferCompleted.
OwnershipTracking guarantees that each Asset has at most 1 owner.
under fair scheduling of approvals, it is guaranteed that
  TransferRequested leads to TransferApproved.

# === Jurisdictional Rules ===
within jurisdiction NL, it is obligatory that
  asset transfers above 10000 EUR require notarial approval
  [BW Art. 3:89].
within jurisdiction NL, it is obligatory that
  vehicle transfers are registered with the RDW
  [Wegenverkeerswet Art. 36].
within jurisdiction EU, it is obligatory that
  cross-border asset transfers are documented for customs
  [EU Regulation 952/2013].

# === Verification Directives ===
verify constraint SingleOwner via z3.
verify temporal AssetTransferProtocol via tla+.
verify process TransferOwnership via mcrl2.

Reading the Program

Let us trace through what this program says, without repeating the language mechanics:

Structure: There are agents, assets, and capabilities. Agents own assets. Assets can be composed. Agents have capabilities that govern what they may do.

Resources: Ownership is linear. When an asset is transferred, the old ownership fact is consumed and a new one is produced. The compiler ensures this bookkeeping is exact.

Space: Assets exist in locations. Locations nest. Transfers are spatially constrained — both parties must be co-located, or the asset must be in transit.

Behavior: Transfers are effects with explicit preconditions and postconditions. Temporal ordering describes what leads to what. Behavioral guarantees specify what the system must ensure under fair scheduling.

Context: The rules specialize by universe. A jurisdiction imposes ownership limits. An organization requires approval for high-value transfers. The same structural definitions apply everywhere — only the constraints tighten.

Verification: Before the program compiles, verification tools check different aspects: logical consistency (Z3), temporal progress (TLA+), and behavioral equivalence (mCRL2). Spatial and probabilistic checking is planned.

Compilation: The verified program is lowered through the compiler's IR, transformed, and translated to Zig. The resulting binary enforces the constraints that survived erasure.

What the Binary Does

The compiled program is not a theorem prover or a model checker. It is a native binary that:

Manages agents, assets, and capabilities as typed data structures
Enforces ownership linearity through move semantics — no garbage collector, no reference counting for ownership facts
Runs seller and buyer processes as concurrent tasks with typed message passing
Scopes data access by spatial containment — a process in one location cannot directly touch assets in another
Reports constraint violations at the boundaries where external input enters the system — the only place where invariants can be threatened at runtime

Everything else — the proofs, the type-level evidence, the erased bindings, the universe hierarchy — exists only at compile time. The binary is lean.

One Language, One Program, One Pipeline

This is the central point of Spine.

A conventional approach to this system would require multiple artifacts: a database schema for facts, an application layer for business logic, a process orchestrator for concurrency, a constraint solver configuration for verification, deployment manifests for spatial concerns, and separate rule engines for jurisdiction-specific policies.

In Spine, it is one program. The facts, the constraints, the effects, the processes, the spatial structure, the resource discipline, the universe hierarchy, the verification targets, and the compilation strategy are all expressed in one language, understood by one compiler, verified by one pipeline, and compiled to one binary.

The developer writes a structured description of the system. The compiler does the rest.

Looking Back

We started this series with a question: what if programming meant describing reality?

Over fourteen posts, we built up the answer piece by piece:

Facts — the world has structure
Rules — structure evolves
Effects — change is explicit
Invariants — some things must always hold
Time — systems evolve
Probability — uncertainty is real
Processes — things happen concurrently
Space — location matters
Resources — usage is tracked
Universes — context determines meaning
Verification — properties are checked
Compilation — descriptions become programs

And now, a complete program that uses all of them.

Spine is still being built. But the shape is clear: a language where you describe the system you mean, and the compiler ensures that what you described is what you get.