A Small Spine Program

Post 3 · Phase 1 — First Example

In the previous post, we introduced facts as the foundation of a system: an agent owns an asset, an asset is part of another asset.

These statements describe what can be true. They define the structure of the problem.

But real systems are not static.

Ownership changes. Permissions evolve. Assets move between contexts.

To model this, we need a way to describe not just what is true, but how truth itself can change.

From Facts to Transitions

Let's return to a concrete statement:

Alice owns a car registered as VIN 12345.

Previously, we expressed this as a fact: Owns(Alice, Car_VIN12345).

Now consider a change: Alice transfers this car to Bob.

In most programming languages, this would be implemented as a mutation — update a field, change a database record.

But this approach focuses on how the change is performed, not on what the change means.

Describing Change

In Spine, we take a different approach.

Instead of describing steps, we describe conditions:

What must be true before a change
What must be true after a change

For ownership transfer, this becomes:

Requires: Alice owns the car
Ensures: Bob owns the car
Ensures: Alice no longer owns the car

This is not an implementation. It is a description of a valid transition.

In Spine's controlled natural language syntax, this looks like:

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.

Each line reads like a sentence, but it is a formal declaration. The compiler knows exactly what requires and ensures mean — they are preconditions and postconditions, not comments.

Rules as First-Class Elements

We can think of this as a rule:

Ownership can be transferred from one agent to another, provided certain conditions hold.

This rule is defined in terms of facts: it consumes existing facts (ownership) and produces new facts (updated ownership).

Importantly, it does not say how to perform the transfer. It defines what a valid transfer is.

The Asset System, Evolving

Our running example now has two layers:

Structure (facts): Owns(Agent, Asset), PartOf(Asset, Asset)
Behavior (rules): Transfer ownership

This separation is intentional.

Facts describe states of the world. Rules describe valid transitions between states.

Valid States, Valid Transitions

Earlier, we introduced constraints such as: an asset has at most one owner.

Now we can see how rules interact with those constraints.

A valid rule must start from a valid state and produce another valid state. This is a genuinely hard problem — there may be constraints that are not obviously affected by a transition. For example, a constraint might say "no person may own more than five cars" — the transfer rule itself doesn't violate single ownership, but it might push the recipient over a limit defined elsewhere in the system.

For example, a transfer rule must not result in multiple owners or no owner at all.

This means: rules are not arbitrary — they are constrained by the structure of the system.

Why This Matters

This way of describing behavior has several consequences.

Clarity

The intent of a rule is explicit — no hidden mutations, no implicit assumptions.

Composability

Rules can be combined and extended: delegation, partial transfers, conditional permissions — all defined in terms of facts.

Reasoning

Because rules are declarative, we can ask: Is a transfer always valid? Can invalid states be reached? Do all transitions preserve constraints?

These questions are difficult to answer when behavior is encoded as arbitrary code.

Not an Implementation (Yet)

At this stage, something important is missing.

We have facts, rules, and constraints. But we do not yet have execution, side effects, or interaction with the outside world.

That is intentional.

We are still describing what changes are allowed — not yet how those changes are carried out.

A Subtle Shift

This introduces another shift in perspective: from writing procedures to describing valid transformations of a system.

Instead of asking "What steps should the program take?", we ask "What must be true before and after any change?"

Looking Ahead

In the next post, we will take the next step: introducing effects, connecting rules to actual operations, and making explicit what a system is allowed to do.

This is where behavior becomes not just described, but structured and constrained as part of the language itself.

And as before, facts remain central: they are the foundation that both rules and effects build upon.