Effects as System Semantics

In the previous post, we introduced rules as descriptions of how a system can evolve: what the system constraints require before a transition, and what they require afterward.

This allowed us to describe valid transitions without committing to a specific implementation.

But something is still missing.

So far, we have described what is true (facts) and how truth can change (rules). We have not yet described what a system is actually allowed to do.

From Rules to Actions

Let's return to our running example.

We defined a rule for transferring ownership: requires current ownership, ensures new ownership.

This describes a valid transformation. But in a real system, something must initiate that transformation — a user action, a system process, an external event.

In most programming languages, this is where we write functions — functions that perform updates, functions that trigger changes. These functions often mix business logic, state mutation, and external interaction.

The result is that it becomes difficult to answer a simple question: What is this system actually allowed to do?

Making Effects Explicit

Languages like Koka show that effects can be made explicit and composable.

Instead of hiding side effects inside functions, they are tracked and described.

Spine takes inspiration from this idea, but places it in a different context.

Effects are not just properties of functions — they are part of the system being modeled.

Effects in the Asset System

In our example, we can introduce an effect: TransferOwnership.

This represents the system's response to a transfer event — the state change that results when an ownership transfer occurs.

Unlike a typical function, this effect is not free-standing. It is constrained by the system: it is only permitted when certain facts hold, and its result must satisfy all system constraints.

In other words: effects are governed by the same structure that defines the system.

Effects and Rules

We can now connect the pieces:

• Facts describe states
• Rules describe valid transitions
• Effects are the system's response to events — the state changes that result from triggering a transition

An effect such as TransferOwnership is the system's response to a transfer event. It is only valid when the rule's conditions are met.

This creates a tight relationship: effects are not arbitrary operations — they are realizations of valid transitions.

Permissions and Capabilities

Once effects are explicit, we can reason about who or what is allowed to trigger them.

For example:

• Only the current owner may transfer an asset
• Delegated agents may have limited permissions

This introduces the idea of capabilities: an agent may have permission to trigger certain effects, and those permissions are themselves part of the system state. Permissions are typically defined over classes — "an owner may sell any car they own" — rather than requiring a separate permission for each individual fact.

Now the system begins to describe not just what changes are valid, but also who is allowed to initiate them.

There is a further subtlety: some permissions may be single-use. A one-time authorization, once exercised, is consumed. This distinction — between resources that persist and resources that are spent — will become important later.

Effects Are Not Just I/O

In many languages, effects are associated with input/output, state mutation, and external systems.

In Spine, effects have a broader role. They describe actions within the system, interactions between agents, and transitions governed by rules.

This shifts the perspective: effects are not just about interacting with the outside world — they are about how the system evolves.

Constraining Behavior

Because effects are explicit and connected to rules, they can be constrained:

• An effect cannot violate invariants
• An effect cannot occur without satisfying preconditions
• An effect cannot produce invalid states

This leads to a powerful property: the space of possible behaviors is structured and limited by the model itself.

Composing Effects

Effects can also be combined: a transfer followed by a delegation, a sequence of operations forming a workflow.

Because each effect is tied to rules and facts, composition remains predictable, analyzable, and constrained.

A Subtle Shift

With effects in place, the system now has three layers:

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

This leads to another shift in perspective: from writing functions that perform actions, to describing systems where actions are first-class and constrained.

Looking Ahead

We now have the core ingredients of a system: structure (facts), transitions (rules), and behavior (effects).

In the next post, we will deepen this further by introducing invariants and guarantees — properties that must always hold.

This will bring us closer to the world of formal reasoning, and connect these ideas to systems like Lean.

At that point, we will not just describe systems and their behavior — we will begin to reason about their correctness.