A Governed Model of Deterministic Program Execution

Conventional execution models allow programs to directly perform effects during evaluation. Even in purely functional languages, effectful computations ultimately resolve into imperative interaction with the external world.

This paper proposes a different default:

Programs do not perform effects. They propose state transitions to a governing runtime.

The runtime adjudicates these proposals against a constitution, executes admissible transitions, and constructs a canonical, append-only ledger of history. Execution becomes not the performance of actions, but the construction of legally admissible history.

Traditional execution assumes:

Evaluate → Perform IO → Continue

Even when IO is abstract (e.g., monadic), the runtime eventually executes it without structural governance beyond sequencing.

In the governed model:

Evaluate → Produce transition proposals → Runtime adjudicates → Apply admissible transitions → Record history

The program is not sovereign. It does not change the world. It computes desired transitions.

A pure function computes outputs solely from inputs. It does not:

• Modify files
• Access the network
• Depend on hidden global state
• Print to the screen

Given identical inputs, it produces identical outputs.

An effect (or transition) is a description of a change to the external world.

In this model:

• Evaluation is purely computational.
• Effects are treated as data.
• Execution is deferred to a governing runtime.

We define:

• State S — abstract representation of the external world
• Proposal P — content-addressed description of a requested transition
• Constitution C — decision function governing admissibility
• Ledger L — canonical append-only record of adjudicated transitions

Execution is defined as:

Program : Input -> [Proposal]
Runtime : (State, Ledger, [Proposal]) -> (State, Ledger)

Programs compute proposals. The runtime constructs admissible history.

Each proposal has a canonical identity derived from its structure:

type ProposalID = Digest SHA256

hashProposal :: TransitionDescription -> ProposalID
hashProposal td =
  hashlazy (canonicalEncode td)

Identity depends only on structure.

If two proposals are structurally identical, they share an ID.

This enables:

• Idempotence
• Symmetry detection
• Deterministic replay
• Content-addressed governance

Identity is not based on time, location in source code, or evaluation order.

The constitution governs admissibility.

data Decision
  = Admit
  | Reject
  | Defer

type Constitution =
  Ledger -> State -> TransitionDescription -> Decision

The constitution has access to:

• Prior history
• Current state
• The proposal

Example:

constitution :: Constitution
constitution ledger state td
  | alreadySucceeded ledger td = Reject
  | violatesPolicy state td    = Reject
  | otherwise                  = Admit

The program cannot bypass this layer. Authority is centralized in the runtime.

Proposals may declare dependencies:

data TransitionDescription = TD
  { tdID           :: ProposalID
  , tdDependencies :: [ProposalID]
  , tdPayload      :: Payload
  }

The runtime constructs a dependency graph and schedules execution in waves:

schedule :: [TransitionDescription]
         -> [[TransitionDescription]]
schedule = topoLayers

Each wave:

• Contains proposals with satisfied dependencies
• May execute in parallel
• Is sorted by ProposalID before recording

Parallel execution does not affect canonical ledger order.

After execution:

currentEntries <- mapConcurrently realizeTransition ready
return (sortOn heEffectID currentEntries ++ nextEntries)

Determinism is preserved despite concurrency.

If dependencies fail, dependent proposals are rejected. Nothing is silently retried or reordered.

Execution consists of adjudication:

executeProposals
  :: Constitution
  -> State
  -> Ledger
  -> [TransitionDescription]
  -> IO (State, Ledger)
executeProposals c st ledger proposals =
  foldM step (st, ledger) proposals
  where
    step (s, l) td =
      case c l s td of
        Reject -> pure (s, appendEntry l td Rejected)
        Defer  -> pure (s, appendEntry l td Deferred)
        Admit  -> do
          s' <- applyTransition s td
          pure (s', appendEntry l td Admitted)

Key properties:

• The program never calls applyTransition.
• Every proposal is recorded.
• Admission decisions are explicit.
• Rejections are first-class outcomes.

Execution becomes iterative construction of admissible history.

Each effect type includes execution and verification:

data EffectSpec = EffectSpec
  { esRun    :: EffectDescription -> IO Outcome
  , esVerify :: EffectDescription -> IO Outcome
  }

The runtime:

1. Decides admissibility.
2. Executes if admitted.
3. Verifies the result.
4. Records the outcome.

Verification ensures that transitions match their declared structure.

The ledger is append-only:

data LedgerEntry = LedgerEntry
  { leID        :: ProposalID
  , leDecision  :: Decision
  , leTimestamp :: UTCTime
  }

type Ledger = [LedgerEntry]

Each entry records:

• Proposal ID
• Dependencies
• Decision
• Outcome
• Constitution version
• Timestamp

Properties:

• No mutation of prior entries
• Deterministic replay under stable constitution
• Automatic idempotence
• Symmetry detection

The ledger is the artifact of execution. Execution is history construction.

To ensure effects remain declarative, effect bodies are restricted.

They may not contain:

isControlFlow (Seq _)       = True
isControlFlow (Let _ _ _)   = True
isControlFlow (Fun _ _ _ _) = True
isControlFlow (If _ _ _)    = True

Effects cannot embed control flow, local bindings, or nested functions.

They are descriptions — not mini-programs.

Decision-making remains in:

• Pure evaluation
• The constitutional runtime

Let:

• f(input) produce proposals P
• C(L, S, p) determine admissibility
• T(S, p) apply transition

Execution:

(S₀, L₀)
  → adjudicate p₁
  → (S₁, L₁)
  → adjudicate p₂
  → (S₂, L₂)
  → ...

If:

• f is deterministic
• C is deterministic
• T is deterministic

Then the resulting ledger is unique.

Execution becomes a deterministic construction of admissible history.

The constitution itself may evolve:

data ConstitutionVersion =
  ConstitutionVersion
    { cvID   :: Digest SHA256
    , cvBody :: Constitution
    }

Each ledger entry records the constitution version used.

Constitutional changes:

• Do not rewrite history
• Apply only to future proposals

History remains stable.

In this model:

A program does not “write a file.”

It proposes:

WriteFile path contents

The constitution decides admissibility. The runtime applies or rejects. The ledger records the outcome.

Programs are petitioners. The runtime is the governing authority.

Imperative model:

Program → Direct effect → World changes

Governed model:

Program → Proposal → Constitutional review → Admissible transition → Recorded history

The difference is structural:

• IO is no longer primitive.
• Governance is mandatory.
• History is intrinsic, not incidental.

This reframing yields:

• Deterministic replay
• Built-in auditability
• Mandatory policy enforcement
• Idempotent execution
• Explicit historical accountability
• Structural separation of intent and realization

The runtime is not a passive executor. It is a governing authority.

This paper presents a governed model of deterministic program execution in which programs do not perform effects but generate content-addressed proposals for state transitions.

A constitutional runtime adjudicates these proposals, executes admissible transitions, and constructs an append-only ledger of canonical history.

Execution is not the performance of action. It is the construction of legally admissible history. Under this model, computing becomes governance.