Resources and Ownership

So far, we have introduced facts, rules, effects, invariants, context, time, space, uncertainty, processes, and spatial structure.

These give us a rich language for modeling systems.

But there is a concept we have used informally without making it precise: some things can only be used once.

Not All Facts Are Equal

Consider our Asset System.

We have the fact: Owns(Alice, Painting).

When Alice transfers the painting to Bob, the system transitions to Owns(Bob, Painting).

But what happened to the original fact? It was not just updated — it was consumed. Alice no longer owns the painting. The old fact is gone, and a new fact takes its place.

This is different from a fact like "the painting is oil on canvas." That fact persists regardless of who owns the painting. It can be observed freely, by anyone, at any time.

These two kinds of facts behave fundamentally differently. The first is a resource — it is consumed when used. The second is persistent — it can be shared without limit.

The Problem of Duplication

In most programming languages, values can be freely copied. A variable holding an ownership record can be duplicated, passed to multiple functions, and referenced from multiple places.

This creates a subtle but important class of errors:

• An ownership token is used twice, causing a double transfer
• A permission is consumed but still referenced elsewhere
• A one-time credential is accidentally shared

These are not logic errors in the traditional sense. They are resource errors — violations of the constraint that certain things should be used exactly once.

Three Modes of Use

Spine addresses this through a concept from Quantitative Type Theory: every binding carries an annotation describing how it may be used.

There are three modes:

• Linear (1) — must be used exactly once. Once consumed, it is gone.
• Unrestricted (ω) — may be used any number of times. This is the familiar default in most languages.
• Erased (0) — exists only at compile time. Used for type information, proofs, and specifications that have no runtime presence.

These are not ad-hoc markers. They are part of the type system itself, checked at compile time.

Resources in the Asset System

Let's return to ownership.

In Spine, the fact Owns(Alice, Painting) is a linear resource. The transfer rule consumes this fact and produces a new one: Owns(Bob, Painting).

Because it is linear, the type system enforces that the original fact cannot be used again after the transfer. There is no way to accidentally create two owners.

Compare this with a fact like Medium(Painting, Oil). This is unrestricted — it can be read, shared, and referenced without affecting the system's state.

Connecting to Effects

Resource tracking integrates naturally with the effect system.

An effect that consumes a resource must account for it. An effect that produces a resource must ensure it is eventually consumed or explicitly discarded.

This creates a discipline: effects are not only constrained by rules and invariants — they are also constrained by resource accounting.

For example: the TransferOwnership effect consumes one ownership fact and produces another. The type system ensures that these balance.

Connecting to Invariants

In earlier posts, we introduced the invariant that an asset has at most one owner.

With resource tracking, this invariant is not just checked — it is structurally enforced.

A linear ownership fact cannot be duplicated. Therefore, two ownership facts for the same asset cannot coexist. The invariant holds not because we test for it, but because the type system makes violation impossible.

This is a significant property: certain invariants become consequences of resource discipline rather than separate proof obligations.

Erased Information

The third mode — erased — plays a different role.

Some information exists only to help the compiler verify correctness. It has no runtime presence and no cost.

For example: a proof that a transfer is valid, type-level evidence that a constraint holds, or specification metadata used during verification.

In Spine, this information can participate in type checking and reasoning without affecting the generated code.

Why Not Just Rust?

Rust introduced ownership and borrowing to mainstream programming, and demonstrated that resource tracking can prevent real bugs.

Spine's approach differs in important ways.

Rust's ownership model is primarily about memory safety — preventing use-after-free, data races, and memory leaks.

Spine's resource tracking is about semantic resources: ownership of assets, consumption of permissions, use of capabilities, and any domain concept where "used exactly once" is meaningful.

The mechanism is also different. Rust uses affine types — values may be used at most once — enforced by a borrow checker. Spine uses Quantitative Type Theory — values are used exactly the number of times their annotation permits — integrated into the dependent type system, which allows richer reasoning about resource flow.

A Subtle Shift

With resource tracking in place, the system gains a new dimension.

Not only do we describe what is true and how truth changes — we describe how many times each piece of truth may be used.

This shifts the perspective once more: from systems where values are freely available, to systems where resources are tracked, consumed, and accounted for.

This is not about restriction for its own sake. It is about making the system's assumptions explicit — and letting the type system enforce them.

Looking Ahead

We now have an even richer foundation: facts, rules, effects, invariants, context, time, space, uncertainty, processes, spatial structure, and resources.

Resource tracking connects to many of the ideas introduced earlier. It strengthens invariants, constrains effects, gives facts a notion of lifetime, and disciplines how processes exchange values across spatial boundaries.

In the next post, we will give structure to the idea of context itself — formalizing the layered interpretations we have been using informally into something precise: universes.