Programming Reality

Most programming languages are built to describe algorithms — sequences of steps that transform data into results.

They are excellent at telling machines what to do.

But many systems we build today are not just algorithms. They are models of the real world.

They describe: who owns what, what is allowed to happen, how systems evolve over time, what must remain true — even as everything changes.

These concerns are often expressed outside of code: in documents, in diagrams, in informal rules, or in the heads of domain experts.

And as a result, a gap emerges between what a system is supposed to be and what the code actually does.

Three Traditions

There is no shortage of deep work addressing parts of this problem.

Formal reasoning, exemplified by systems like Lean, shows how far we can push the ability to prove that a program meets its goals — that certain properties always hold and certain errors can never occur.

Fact-based modeling, such as Object-Role Modeling (ORM2), provides a way to describe a business problem in terms of relationships and constraints that are easy to understand and validate — structure, not algorithms.

Explicit state changes, as explored in languages like Koka, demonstrate how the ways a system can change — what traditional developers might call transactions — can be made visible, composable, and tractable.

Each of these traditions is powerful in its own right.

But they largely exist in isolation: reasoning is separated from execution, modeling is separated from behavior, effects are separated from domain constraints.

A Missing Layer

What is still missing is a way to bring these perspectives together into a single system.

A system where:

• Facts describe the structure of a business problem
• Constraints express what must always be true
• Transitions describe how the system can evolve

And where all of these can be executed, analyzed, and verified together.

This is the space Spine explores.

What Is Spine?

Spine is a programming language for modeling and constructing systems where correctness is not an afterthought.

It is built around a simple idea:

Programs should describe not only what happens, but what must always be true as a system evolves.

To support this, Spine brings together:

• Fact-based modeling, inspired by Object-Role Modeling — represent the possible states of the world, then talk about transitions
• Formal reasoning, in the spirit of Lean — prove that the program meets its goals
• Explicit state changes, following ideas explored in Koka — make every system transition visible and constrained

But it does not aim to replace these systems.

Instead, it explores what happens when their ideas are combined, extended, and made executable.

From Description to Execution

In many systems today, there is a sharp boundary between modeling a problem, implementing behavior, and verifying correctness.

Spine attempts to blur this boundary.

A model is not just documentation. A rule is not just a comment. A constraint is not just an assumption.

They are all part of the program.

And because they are part of the program, they can be executed, checked, composed, and verified.

A Different Perspective on State Changes

In most programming languages, state changes answer the question: "What does this function do?"

In Spine, the question shifts slightly: "What kinds of changes are possible in this system?"

State changes are not just annotations on functions — they are part of how system behavior is described and constrained.

A Note on Scope

Spine is an ongoing exploration.

It draws from established ideas, but it does not claim to replace them. It is not a theorem prover, though it borrows from that world. It is not a modeling methodology, though it builds on one. It is not just an effect system, though effects play a central role.

Instead, it sits at their intersection.

Looking Ahead

In the coming posts, we will explore:

• How facts can become first-class elements of a program
• How effects interact with system constraints
• How logic and execution can coexist
• How real-world dimensions like time and uncertainty can be modeled directly
• How programs can be compiled through a pipeline that includes formal verification

The goal is not just to introduce a language, but to explore a different way of thinking about programs.

Not just as instructions for machines, but as structured descriptions of systems that must remain coherent over time.