Dependent Types and Real-World Systems

So far, we have built up a small but expressive foundation:

• Facts describe what is true
• Rules describe how truth can change
• Effects describe what actions are possible

This already allows us to model systems in a structured way.

But an important question remains: How do we ensure that certain properties always hold?

For example: an asset should never have more than one owner, a transfer should not create invalid states, and permissions should remain consistent.

We can state these informally. But we want more than that. We want these properties to be part of the system itself.

From Constraints to Guarantees

In earlier posts, we introduced constraints: "An asset has at most one owner."

These constraints define what valid states look like.

Now we take the next step: expressing properties that must hold across all possible states and transitions.

This moves us from describing valid configurations to reasoning about entire systems.

A Glimpse of Dependent Types

Systems like Lean and Idris show how types can be used to express precise properties.

In these systems, types are not just categories like integers or strings. They can express relationships and constraints.

For example, a type might encode "a list of length n" or "a value greater than zero".

This is the essence of dependent types: types that depend on values, and can express detailed properties about them.

Bringing This Into Systems

Spine draws inspiration from these ideas, but applies them in a different setting.

Instead of focusing primarily on mathematical objects or isolated functions, we are dealing with evolving systems, facts and relationships, and actions over time.

The question becomes: How can we express properties of an entire system in a precise way?

Invariants in the Asset System

Let's return to our example.

We already have the idea that an asset has at most one owner. In Spine, this is not just a guideline. It is part of the system's fact model — a constraint defined alongside the facts themselves, not layered on after the code is written.

It applies to all states, across all transitions, regardless of which effects are used.

This kind of property is often called an invariant.

Rules Must Preserve Invariants

Once invariants are part of the system, they impose obligations.

For example: the transfer rule must not create multiple owners. No sequence of effects should violate ownership uniqueness.

This leads to an important shift: it is not enough for a rule to describe a change — it must preserve the correctness of the system.

From Local Checks to Global Reasoning

In many programs, correctness is enforced through tests, runtime checks, and careful discipline.

These approaches are useful, but they are partial and external to the program's structure.

In a system with richer types and constraints, we can instead ask:

• Are there any sequences of actions that break the rules?
• Can an invalid state ever be reached? (This is NP-complete in the general case — which is precisely why tools like TLA+ exist: they search the state transition space to find any sequence of transitions that results in a constraint being violated.)
• Do all allowed transitions preserve invariants?

These are not just runtime questions — they are questions about the system itself.

There is a further subtlety: some meaningful constraints can be stated but not evaluated until after a violation has occurred. For example, "the transfer of ownership must be notified to the authority within two weeks" cannot be checked until the deadline has passed. These temporal constraints require different treatment from the static invariants above.

Expressing Properties of Behavior

We can now start to express properties like:

• "Ownership is always unique"
• "Every transfer results in a valid state"
• "Unauthorized actions cannot occur"

These are not tied to a single function or operation. They describe the behavior of the system as a whole.

Some of these properties go beyond logical correctness. For instance, we may want to express that resources are never duplicated or lost — that every transfer accounts for what is consumed and what is produced. This kind of guarantee involves not just what is true, but how many times each fact is used.

Not Just Mathematics

At this point, it might seem like we are moving toward a theorem prover.

Systems like Lean are extremely powerful in expressing and proving properties.

Spine shares some of this foundation, but has a different focus. It is not primarily about proving abstract theorems. Instead, it is about modeling real systems, expressing their constraints, and ensuring those constraints are respected.

Bridging Description and Guarantee

What makes this interesting is the combination:

• Facts describe structure
• Rules describe change
• Effects describe behavior
• Types and invariants describe correctness

These are not separate layers. They are all part of the same system.

A Subtle Shift

This leads to another shift in perspective: from writing programs that try to be correct, to describing systems where correctness is part of their structure.

Instead of asking "Did we handle all edge cases?", we can ask "Is it even possible to construct an invalid state?"

Looking Ahead

We now have structure, behavior, constraints, and guarantees.

In the next post, we will bring these elements together: how facts, rules, effects, and invariants interact, how they form a coherent whole, and how this differs from traditional approaches.

At that point, the shape of Spine as a unified system will start to become clear.