Spine in 15 Minutes

The previous sixteen articles explain why Spine works the way it does. This article shows what you write and what happens when you compile it. No category theory. No proof theory. Just syntax, compiler behavior, and output.

What Spine Is

Spine is a language for describing systems — what things exist, how they can change, and what must always be true. The compiler reads those descriptions and produces two things: native code (via Zig) and verification artifacts (Z3, TLA+, mCRL2). You write one source file. The compiler decides which parts need runtime code and which parts need proofs.

1. Data and Functions

Spine has algebraic data types and pattern matching. If you know Haskell or ML, this will look familiar.

data Maybe a : Type where
  Nothing : Maybe a
  Just    : a -> Maybe a

data List a : Type where
  Nil  : List a
  Cons : a -> List a -> List a

record Person where
  field name  : String
  field age   : Nat
  field email : String

Functions use equation-style definitions with pattern matching:

factorial : Nat -> Nat
factorial 0 = 1
factorial n = n * factorial (n - 1)

add : Int -> Int -> Int
add x y = x + y

compose : (b -> c) -> (a -> b) -> a -> c
compose f g x = f (g x)

This compiles to Zig. A record becomes a Zig struct. A data becomes a tagged union. Pattern matching becomes branching. Here is an actual compiler output fragment — the lexer's token type, from lexer.model:

-- Source (lexer.model):
enum TokenType =
    INT | FLOAT | STRING | CHAR | BOOL
  | DEF | LET | IN | IF | THEN | ELSE
  | MATCH | CASE | OF | DATA | ENUM
  | RECORD | TYPE | MODULE | WHERE
  | IMPORT | EXPORT | EXTERNAL
  | CLASS | INSTANCE | INDUCTIVE | FORALL
  | PLUS | MINUS | STAR | SLASH ...

record Token where
  kind   : TokenType
  value  : String
  line   : Int
  column : Int

// Generated (lexer.zig):
pub const TokenType = enum {
    INT, FLOAT, STRING, CHAR, BOOL,
    DEF, LET, IN, IF, THEN, ELSE,
    MATCH, CASE, OF, DATA, ENUM,
    RECORD, TYPE, MODULE, WHERE,
    IMPORT, EXPORT, EXTERNAL,
    CLASS, INSTANCE, INDUCTIVE, FORALL,
    PLUS, MINUS, STAR, SLASH, ...
};

pub const Token = struct {
    kind: TokenType,
    value: []const u8,
    line: i64,
    column: i64,
    length: i64,
};

The compiler that produced this Zig is itself written in Spine (145 modules). It compiles its own source through its own pipeline — that is what self-hosting means here.

2. Effects

Spine has algebraic effects. An effect declares operations; a handler says what those operations do.

effect State s where
  get : State s s
  put : s -> State s Unit

effect Console where
  readLine : Console String
  printLine : String -> Console Unit

effect Error e where
  throw : e -> Error e a

Handlers are separate from effect declarations:

handler constReader where
  get _ k -> k 42
  put _ k -> k ()

Effects can carry correctness properties. These are not comments — the compiler extracts them for verification:

constraint GetPutLaw {
  description: "get >>= put ≡ return ()"
  predicate: "forall handler in StateHandler, s in State :
    (perform get >>= \x -> perform (put x)) ≡ return Unit"
}

constraint PutPutLaw {
  description: "put x >> put y ≡ put y"
  predicate: "forall handler in StateHandler, x in s, y in s :
    (perform (put x) >> perform (put y)) ≡ perform (put y)"
}

3. Type Classes

Type classes work as you would expect from Haskell, with one addition: Spine's type system is dependently typed, so class constraints can express richer properties.

class Eq a where
  eq  : a -> a -> Bool
  neq : a -> a -> Bool
  neq x y := not (eq x y)

class Functor f where
  fmap : (a -> b) -> f a -> f b

class Functor m => Monad m where
  unit : a -> m a
  bind : m a -> (a -> m b) -> m b

instance Eq Color where
  eq Red   Red   = true
  eq Green Green = true
  eq Blue  Blue  = true
  eq _     _     = false

4. Behavior: State Machines

This is where Spine diverges from general-purpose functional languages. A behavior block declares a state machine — states, transitions, guards, and message sends.

behavior ActorLifecycle where
  state Spawned [initial]
  state Ready
  state Running
  state Waiting
  state Stopped [final]
  state Crashed [final]

  on Enqueue         : Spawned → Ready
  on Schedule        : Ready → Running
  on ProcessComplete : Running → Ready
    guard (has_messages)
  on ProcessComplete : Running → Waiting
    guard (no_messages)
  on Enqueue         : Waiting → Ready
  on Shutdown        : Running → Stopped
  on Shutdown        : Ready → Stopped
  on Shutdown        : Waiting → Stopped
  on Exception       : Running → Crashed

This is the lifecycle of every actor in Spine's own runtime — the system models itself using its own syntax. Transitions can send messages to other state machines:

behavior Supervisor where
  state Booting [initial]
  state SpawningActors
  state Running
  state ShuttingDown
  state Stopped [final]

  on Start          : Booting → SpawningActors
  on AllSpawned     : SpawningActors → Running
  on ShutdownSignal : Running → ShuttingDown
    send Registry.Shutdown
    send Storage.Shutdown
    send HTTP.Shutdown
    send PG.Shutdown
  on AllStopped     : ShuttingDown → Stopped

The compiler translates behaviors into mCRL2 process algebra for model checking. Here is the actual generated output from a wafer processing example:

-- Source (groote_demo.model):
behavior WaferCycleSpec where
  state Idle [initial]
  state Loading
  state Aligning
  state Exposing
  state Measuring
  state Unloading

  on load    : Idle → Loading
  on align   : Loading → Aligning
  on expose  : Aligning → Exposing
  on measure : Exposing → Measuring
  on unload  : Measuring → Unloading
  on done    : Unloading → Idle

% Generated (groote_demo.mcrl2):
sort State_WaferCycleSpec = struct
  Idle | Loading | Aligning
  | WCS_Exposing | WCS_Measuring | WCS_Unloading;

act align, begin_measurement, check_quality,
    coarse_align, cycle_done, done, eject_wafer,
    end_expose, expose, fine_align, load,
    load_wafer, measure, unload, verify_align;

proc WaferCycleSpec(s: State_WaferCycleSpec) =
  (s == Idle)           -> load . WaferCycleSpec(Loading) +
  (s == Loading)        -> align . WaferCycleSpec(Aligning) +
  (s == Aligning)       -> expose . WaferCycleSpec(WCS_Exposing) +
  (s == WCS_Exposing)   -> measure . WaferCycleSpec(WCS_Measuring) +
  (s == WCS_Measuring)  -> unload . WaferCycleSpec(WCS_Unloading) +
  (s == WCS_Unloading)  -> done . WaferCycleSpec(Idle);

The mCRL2 output is not a pretty-printed version of the source. It is a process algebra specification that the mCRL2 toolset can model-check for deadlock freedom, liveness, and bisimulation equivalence.

5. Catching Bugs: Simulation Refinement

Suppose an engineer adds a shortcut — skip_alignment — that bypasses alignment and goes straight to exposure. The spec says alignment always precedes exposure. How does the compiler catch this?

The implementation declares the shortcut:

behavior WaferCycleImpl where
  state WaitingForWafer [initial]
  state PreAlignment
  state FineAlignment
  state AlignmentVerified
  state PreExposure
  state Exposing
  ...

  on load_wafer     : WaitingForWafer → PreAlignment
  on coarse_align   : PreAlignment → FineAlignment
    send Aligner.StartAlignment
  on fine_align     : FineAlignment → AlignmentVerified
  on skip_alignment : PreAlignment → PreExposure   -- the shortcut
  on start_expose   : PreExposure → Exposing
    send ExposureUnit.BeginExposure
  ...

You declare a refinement mapping between the implementation and the spec:

simulation WaferRefinement : WaferCycleImpl refines WaferCycleSpec where
  map WaitingForWafer   = Idle
  map PreAlignment      = Loading
  map FineAlignment     = Aligning
  map AlignmentVerified = Aligning
  map PreExposure       = Aligning
  map Exposing          = Exposing
  ...

  on load_wafer     : matches load
  on coarse_align   : matches align
  on fine_align     : internal
  on skip_alignment : internal
  on start_expose   : matches expose
  ...

The skip_alignment transition maps PreAlignment → PreExposure, which in spec-space maps Loading → Aligning. An internal transition (one with no spec counterpart) requires source and target to map to the same spec state. Loading ≠ Aligning. The simulation checker flags this as a refinement violation.

This check happens statically, through the generated mCRL2 model. The mCRL2 toolset verifies whether the implementation is a weak bisimulation of the spec. The shortcut breaks that relation.

6. Spatial Structure

Spine can model physical containment and topology using region blocks. This is relevant for systems where where something is affects what it can do.

region WaferStage where
  sort equipment_sort

region Aligner where
  sort equipment_sort

region ExposureUnit where
  sort equipment_sort

region LithoCell where
  contains WaferStage, Aligner, ExposureUnit, MeasurementUnit
  links control : ControlBus, wafer_in : WaferPort, wafer_out : WaferPort
  sort machine_sort

region CleanRoom where
  contains LithoCell
  links transport : TransportBus
  sort facility_sort

Spatial rewrites describe how the topology can change:

react add_litho_cell where
  redex CleanRoom
  reactum CleanRoom, LithoCell

If a rewrite references a region that does not exist — say, CoolingUnit without a prior declaration — the compiler catches it. The spatial model compiles to BigraphER for topological verification.

7. Temporal Properties and Z3 Laws

Temporal claims and arithmetic laws live in the same source file as the rest of the system.

temporal StageStability where
  always stage_locked_during_exposure
  over WaferStage, ExposureUnit

temporal WaferCompletion where
  eventually wafer_processed
  over LithoCell

temporal LoadToMeasure where
  wafer_loaded leads_to wafer_measured
  over WaferStage, MeasurementUnit

Temporal properties are compiled to TLA+ for model checking. Arithmetic laws go to Z3:

-- Z3 proves this:
law wafer_throughput_positive :
  ∀ (n : Int). n > 0 → n * 1 > 0

-- Z3 refutes this:
law bad_throughput_claim :
  ∀ (x y : Int). x + y > x

The compiler dispatches each claim to the appropriate solver. You do not write Z3 assertions or TLA+ specs by hand. You write Spine. The compiler decides what goes where.

8. The Controlled Natural Language Surface

Everything above uses Spine's functional syntax — the fragment closest to Haskell or ML. Spine also has a controlled natural language (CNL) surface for domain modeling:

Person has exactly 1 LastName.

Engine is part of Car.

it is obligatory that each Asset has at most 1 owner.

it is forbidden that an Agent transfers an Asset it does not own.

TransferRequested leads to TransferApproved.

within jurisdiction NL, it is obligatory that asset transfers
above 10000 EUR require notarial approval [BW Art. 3:89].

This is not a separate language. The CNL surface is a fragment — a set of grammar rules that expand the parser's vocabulary. Internally, the sentence Person has exactly 1 LastName lowers to the same typed representation as a record field constraint. The deontic modalities (obligatory, forbidden, permitted) lower to temporal and constraint annotations that the compiler dispatches to the appropriate verifier.

The CNL exists because the people who know the domain rules — lawyers, engineers, compliance officers — do not write Haskell. The functional syntax and the CNL surface compile through the same pipeline to the same IR.

How the Pieces Fit Together

A single Spine source file can contain data declarations, functions, effects, behaviors, spatial structure, temporal properties, Z3 laws, and CNL facts. The compiler reads the file and does the following:

1. Parse all fragments. The parser handles functional syntax, behavior blocks, region blocks, temporal declarations, and CNL sentences.
2. Lower everything to a shared intermediate representation — a graph of primitive operations.
3. Partition the graph. Constraint subgraphs go to Z3. Temporal and behavioral subgraphs go to TLA+ and mCRL2. Spatial subgraphs go to BigraphER. The computational subgraph goes to Zig.
4. Emit artifacts for each backend. The Zig output compiles to a native binary. The verification artifacts are checked by their respective tools.

The compiler does not do all of this because it is clever. It does it because the IR makes partitioning a structural operation — different subgraphs, same graph.

What Exists Today

The compiler is self-hosting: 145 modules (lexer, parser, type checker, code generator, verification dispatch) written in Spine, compiled by the Spine compiler, producing Zig. The pipeline works for the functional fragment, behavior fragment, and constraint dispatch. The spatial and probabilistic backends are at an earlier stage.

Spine is not packaged for public use yet. This article and the article series document the design. The Discord is the best place to ask questions or see updates.