eventcore-kernel.md

Excellent. This is a superb prompt. You have a solid, well-reasoned algebraic theory. My task is to refine it into a canonical specification, tightening the definitions, ensuring completeness (especially for the CQRS aspect, which is implied but not fully specified), and then using that specification to derive a high-level language kernel and syntax that would make programming in this paradigm a natural extension of the theory.

The result will be a two-part document:

1. The Core Algebraic Theory: A formal specification of the sorts, operations, and axioms for both the command and query/projection sides of the system.
2. The Axiom Language Kernel: A high-level language design and syntax that provides first-class constructs for the concepts defined in the theory, making the boilerplate minimal and the business logic central.

---

Part 1: A Refined Algebraic Theory of EventCore

This specification formalizes the semantics of a multi-stream, aggregateless event-sourcing system.

1. Sorts (Core Types)

• Event: The set of domain events.
• Command: The set of commands representing intent.
• State: The set of command-specific, in-memory states.
• InitialState: A distinguished constant, InitialState ∈ State, representing the default starting state for any reconstruction.
• StreamId: A set of unique stream identifiers.
• EventId: A totally ordered set of unique, chronologically sortable event identifiers.
• EventVersion: The set of natural numbers ℕ₀, where 0 represents the state of a non-existent stream.
• StoredEvent: A tuple (id: EventId, stream: StreamId, version: EventVersion, event: Event).
• Stream: A sequence of StoredEvents, Seq<StoredEvent>, strictly ordered by EventVersion.
• EventStore: A map from stream identifiers to streams, StreamId → Stream.
• Conflict: A special value indicating an optimistic concurrency failure.
• WriteOp: A tuple (StreamId, Event).

Sorts for Projections (Read-Side):

• ReadModel: The set of query-optimized read models.
• ReadModelId: A set of unique read-model identifiers.
• ReadModelStore: A map from read-model identifiers to read models, ReadModelId → ReadModel.
• Checkpoint: An optional event identifier, Maybe<EventId>, tracking a projection's progress.
• Query: A specification for retrieving data from the ReadModelStore.
• Projection: A pair of functions defining read-model logic:
  • which_model: StoredEvent → Maybe<ReadModelId>
  • project: Maybe<ReadModel> × StoredEvent → Maybe<ReadModel>

2. Operations (Functions)

Command-Side Operations:

• initial_streams: Command → Set<StreamId>
  • Returns the initial set of streams a command must read.
• apply: State × StoredEvent → State
  • The pure state transition function for command-side state reconstruction.
• handle: Command × State × Set<StreamId> → Either<Set<StreamId>, Seq<WriteOp>>
  • The decision-making function. Left requests more streams; Right issues writes.
• read: EventStore × Set<StreamId> → (Seq<StoredEvent>, Map<StreamId, EventVersion>)
  • Reads events from a set of streams, returning them sorted by EventId, along with the latest version of each stream.
• write: EventStore × Map<StreamId, EventVersion> × Seq<WriteOp> → Either<Conflict, EventStore>
  • Atomically appends events to streams, conditional on the provided versions.

Projection-Side Operations:

• events_after: EventStore × Checkpoint → Seq<StoredEvent>
  • Returns all events from the EventStore after the given checkpoint, sorted by EventId.
• run_projection: Projection × EventStore × ReadModelStore × Checkpoint → (ReadModelStore, Checkpoint)
  • Updates a ReadModelStore by processing new events from the EventStore.
• query: ReadModelStore × Query → Seq<ReadModel>
  • Executes a query against the ReadModelStore.

3. Axioms (Laws)

Command-Side Axioms:

1. State Reconstruction is a Fold: The reconstruction of state is a left fold over chronologically sorted events. reconstruct(events) ≜ fold_left(apply, InitialState, sort_by_id(events))

2. Write Boundary Integrity: A command can only decide to write to streams that are part of its current consistency boundary. handle(cmd, state, boundary) = Right(writes) ⇒ {s | (s, e) ∈ writes} ⊆ boundary

3. Core Execution Loop: The execute function is defined by a bounded recursion that expands the consistency boundary. execute(store, cmd) ≜ execute'(store, cmd, initial_streams(cmd), N) where N is a constant iteration limit. execute'(store, cmd, boundary, n) where n > 0:

   let (events, versions) = read(store, boundary) in
   let state = reconstruct(events) in
   match handle(cmd, state, boundary) with
     | Left(new_streams)  -> execute'(store, cmd, boundary ∪ new_streams, n - 1)
     | Right(writes)      -> write(store, versions, writes)
   

   execute'(store, cmd, boundary, 0) ≜ Left(Conflict)

4. Optimistic Concurrency: A write fails if any expected stream version does not match the actual version in the store. write(store, expected, writes) = Left(Conflict) if ∃ s ∈ dom(expected) such that latest_version(store, s) ≠ expected[s].

5. Atomic & Consistent Writes: If a write succeeds, all events are appended atomically with correctly incremented versions. If write(store, versions, writes) = Right(store'), then for each (s_id, event) ∈ writes, a new StoredEvent e_new exists in store' such that:

   • e_new.version = latest_version(store, s_id) + 1
   • stream(store', s_id) = append(stream(store, s_id), e_new)
   • All such appends are an atomic unit of change from store to store'.

6. Event Immutability: The event store is append-only. If store' = write(store, ...), then ∀s ∈ dom(store), stream(store, s) is a prefix of stream(store', s).

Projection-Side Axioms:

7. Projection is a Fold: The run_projection operation is a left fold over new events, applying each to the ReadModelStore. run_projection(proj, store, rm_store, chk) ≜

   let new_events = events_after(store, chk) in
   fold_left(
     (acc_rm_store, event) => apply_event_to_store(proj, acc_rm_store, event),
     rm_store,
     new_events
   )
   

   ...where apply_event_to_store uses proj.which_model and proj.project to update the store for a single event. The final checkpoint is the ID of the last event processed.

8. Idempotency: Re-running a projection over the same events yields the same ReadModelStore. run_projection(proj, store, initial_rm_store, chk).0 ≡ run_projection(proj, store, run_projection(proj, store, initial_rm_store, chk).0, chk).0

9. Command-Query Responsibility Segregation (CQRS): The command and query sides are formally separated.

   • execute is the only operation that can produce a new EventStore.
   • run_projection is the only operation that can produce a new ReadModelStore.
   • query operations are read-only on the ReadModelStore.
   • execute does not read from the ReadModelStore, and run_projection does not write to the EventStore.

---

Part 2: The Axiom Language Kernel & Syntax

This section proposes a high-level, declarative language named Axiom designed to make the algebraic theory its native execution model. The syntax is designed to be horizontally decomposed, making the command the central, minimally-boilerplate unit of work by factoring out reusable state-building logic.

Core Concept: The view

A view is a reusable, pure definition for reconstructing a command-specific state model from an event stream. It encapsulates the state schema and the apply logic.

// A reusable view to calculate the balance of a single bank account.
view AccountBalance {
  // 1. Defines the data structure for the state. Defaults are provided.
  state {
    balance: Money = 0,
    is_open: bool = false,
  }

  // 2. Defines the fold/apply logic.
  // 'self' refers to the state being built.
  on BankingEvent {
    match event {
      AccountOpened { initial_balance } => update {
        balance: initial_balance,
        is_open: true
      },
      Deposited { amount } => update {
        balance: self.balance + amount
      },
      Withdrawn { amount } => update {
        balance: self.balance - amount
      },
      AccountClosed {} => update {
        is_open: false
      }
    }
  }
}

The command: Central Decision Logic

The command syntax focuses purely on the decision-making (handle) logic. It declaratively states its data dependencies using views, and the runtime handles the rest.

// The command is lean and centered on business logic.
command TransferMoney(from: AccountId, to: AccountId, amount: Money)
// The 'using' clause declaratively builds the command's consistency boundary and state.
using
  // Bind the 'AccountBalance' view to the 'from' stream, making the result available as 'from_acct'.
  from_acct: AccountBalance on stream "account-{from}",
  // Bind the 'AccountBalance' view to the 'to' stream, available as 'to_acct'.
  to_acct: AccountBalance on stream "account-{to}"
{
  // The 'decide' block is the implementation of the `handle` operation.
  // The runtime provides 'from_acct' and 'to_acct' as fully reconstructed state records.
  decide {
    // Business rules are expressed with a first-class `require` keyword.
    require from_acct.is_open, "Source account is closed";
    require to_acct.is_open, "Destination account is closed";
    require from_acct.balance >= amount, "Insufficient funds";

    // Dynamic stream discovery is a first-class keyword.
    // This triggers the re-read/re-execute loop from Axiom 3.
    if amount > 10_000 {
      let approval_stream = discover stream "approvals";
      emit RequiresApproval { from, to, amount } on approval_stream;
    }

    // The 'emit' keyword produces a WriteOp.
    // The compiler enforces Axiom 2: writes can only occur on streams
    // declared in the `using` clause or via `discover`.
    emit Withdrawn { amount } on stream "account-{from}";
    emit Deposited { amount } on stream "account-{to}";
  }
}

How the Syntax Maps to the Theory:

• view: Encapsulates State, InitialState, and the apply operation.
• command ... using ... on stream: Implements the initial_streams operation. The compiler collects all stream declarations into the initial set.
• The Runtime + using: The runtime automatically performs the read and reconstruct operations before executing the decide block.
• decide { ... }: The body of the handle operation.
• discover stream "...": The language construct for returning Left(new_streams).
• emit ... on ...: The language construct for returning Right(writes).
• require ...: Syntactic sugar for a common decision pattern (early exit with an error).

The Read Side: readmodel and projection

The horizontal decomposition extends to the read side, separating the data schema (readmodel) from the transformation logic (projection).

// 1. The Read Model: a data-only schema definition with query hints.
readmodel AccountSummary {
  @primary id: string,
  @index owner: string,
  balance: Money,
  last_activity: datetime,
  status: string,
}

// 2. The Projection: a stream of logic that populates the read model.
projection AccountUpdater for AccountSummary from BankingEvent {
  // Implements `which_model`: maps an incoming event to a specific read model instance.
  maps event to readmodel by event.stream_id

  // Implements `project`: the pure state transition logic.
  // 'self' refers to the existing read model instance (Maybe<ReadModel>).
  on event {
    match event {
      AccountOpened { owner, initial_balance } => {
        // Creates a new read model instance.
        create {
          id: event.stream_id,
          owner,
          balance: initial_balance,
          last_activity: event.timestamp,
          status: "Open"
        }
      },
      Deposited { amount } | Withdrawn { amount } => {
        // Updates an existing instance.
        update {
          balance: if (event is Deposited) then self.balance + amount else self.balance - amount,
          last_activity: event.timestamp
        }
      },
      AccountClosed {} => {
        update {
          status: "Closed",
          last_activity: event.timestamp
        }
      }
    }
  }
}

This comprehensive specification provides a robust, provably correct foundation (the theory) and a developer-friendly, high-level programming model (the Axiom language) that are perfectly aligned. The language syntax directly guides developers to write code that is correct by construction according to the axioms of the underlying theory.

gistfile1.txt

Here is a description and specification of the eventcore semantics, capturing its fundamental execution and storage model as a purely functional algebraic theory.

---

### An Algebraic Theory of EventCore Semantics

This document specifies the semantics of `eventcore` as a purely functional algebraic theory. It defines the core types (sorts), the functions that operate on them (operations), and the laws that govern their behavior (axioms). This model is "aggregateless" and "multi-stream," where consistency boundaries are defined dynamically by commands rather than by a predefined aggregate structure.

#### 1. Overview of the Model

The core execution model is a pure function, `execute`, which takes the current state of the world (the `EventStore`) and a `Command`, and produces a new `EventStore`. This process is defined by a "read-reconstruct-decide-write" flow with two important extensions:

1.  **Dynamic Consistency Boundaries**: A command can dynamically request to read from additional event streams during its execution, causing the process to re-read and re-execute with the expanded set of streams.
2.  **Optimistic Concurrency**: Writes are conditional on the versions of the streams read, ensuring atomic and consistent updates across multiple streams. A version mismatch results in a conflict, which is typically handled by retrying the entire `execute` function.

#### 2. Sorts (Core Types)

The theory is defined over the following sorts (types):

*   **`Event`**: The set of all possible domain events. These are the facts or state changes that have occurred.
*   **`State`**: The set of all possible states. A `State` is a temporary, in-memory representation derived from events, specific to a `Command`.
*   **`Command`**: The set of all possible commands. A `Command` represents an intent to change the system's state.
*   **`StreamId`**: The set of unique identifiers for event streams.
*   **`EventId`**: The set of globally unique, chronologically ordered event identifiers. This set has a total order `<`.
*   **`EventVersion`**: The set of natural numbers (`ℕ`), representing the version of an event within a single stream.
*   **`StoredEvent`**: The canonical representation of a persisted event, defined as a tuple:
    `StoredEvent ::= (id: EventId, stream: StreamId, version: EventVersion, event: Event)`
*   **`Stream`**: An ordered sequence of `StoredEvent`s: `[StoredEvent]`. Events within a stream are strictly ordered by `EventVersion`.
*   **`EventStore`**: The state of the entire storage system, modeled as a map from `StreamId` to `Stream`:
    `EventStore ::= Map<StreamId, Stream>`
*   **`ConsistencyBoundary`**: A set of stream identifiers: `{StreamId}`.
*   **`WriteOp`**: An event to be written to a specific stream: `(StreamId, Event)`.
*   **`Conflict`**: A special value indicating an optimistic concurrency failure.
*   **`Maybe<T>`**: Represents an optional value, equivalent to `T | Nil`.
*   **`Either<A, B>`**: Represents a value that is either of type `A` or type `B`.

#### 3. Operations (Functions)

The semantics are defined by the following pure functions:

*   **`initial_streams`**: `Command → ConsistencyBoundary`
    *   Defines the initial set of streams a command needs to read to make a decision.

*   **`apply`**: `State × StoredEvent → State`
    *   The state transition function (a fold). It applies a single event to an existing state to produce a new state.

*   **`handle`**: `Command × ConsistencyBoundary × State → Either<[StreamId], [WriteOp]>`
    *   The decision-making function. Given the command, the current set of streams being considered (`ConsistencyBoundary`), and the state reconstructed from those streams, it decides what to do next.
    *   It returns `Left([StreamId])` if it needs to read from additional streams to make a decision.
    *   It returns `Right([WriteOp])` if it has sufficient information and decides to produce new events.

*   **`read`**: `EventStore × ConsistencyBoundary → ([StoredEvent], Map<StreamId, EventVersion>)`
    *   Reads from the event store. Given a set of streams to read, it returns:
        1.  A single list of all `StoredEvent`s from those streams, sorted chronologically by `EventId`.
        2.  A map containing the latest `EventVersion` for each stream read. If a stream does not exist, its version is considered `0`.

*   **`write`**: `EventStore × Map<StreamId, EventVersion> × [WriteOp] → Either<Conflict, EventStore>`
    *   Writes to the event store atomically. Given the current store, a map of expected stream versions, and a list of new events to write, it either:
        1.  Returns `Left(Conflict)` if any of the expected versions do not match the actual latest versions in the store.
        2.  Returns `Right(EventStore')`, the new state of the store after atomically appending the new events to their respective streams and assigning them new `EventId`s and `EventVersion`s.

*   **`reconstruct`**: `[StoredEvent] → State`
    *   A helper function that reconstructs state from a list of events. It is defined in terms of `apply`.

#### 4. Axioms (Laws)

The behavior of the operations is governed by the following axioms:

1.  **State Reconstruction is a Fold:**
    `reconstruct(events) ≡ fold_left(apply, initial_state, sort_by_id(events))`
    *   State is always derived by applying events chronologically, starting from a default initial state. `sort_by_id` sorts events by their `EventId`.

2.  **Type-Safe Writes:**
    For any `cmd`, `boundary`, `state`:
    `handle(cmd, boundary, state) = Right(writes) ⇒ {s | (s, e) ∈ writes} ⊆ boundary`
    *   A command can only decide to write events to streams that are part of its current `ConsistencyBoundary`. This is the algebraic equivalent of the `ReadStreams`/`StreamWrite` compile-time guarantee.

3.  **Core Execution Loop with Dynamic Discovery:**
    The primary `execute` function is defined recursively to model the dynamic discovery of streams. It is parameterized by a maximum number of iterations `N` to guarantee termination.
    `execute(store, cmd) ≡ execute'(store, cmd, initial_streams(cmd), N)`

    `execute'(store, cmd, boundary, n)` where `n > 0`:
    ```
    let (events, versions) = read(store, boundary)
    let state = reconstruct(events)
    let decision = handle(cmd, boundary, state)
    
    match decision:
      case Left(new_streams):
        // Re-execute with the expanded boundary
        execute'(store, cmd, boundary ∪ new_streams, n - 1)
      
      case Right(writes):
        // Final decision, attempt to write
        write(store, versions, writes)
    ```
    `execute'(store, cmd, boundary, 0) ≡ Left(Conflict)`
    *   This specifies that execution begins with an initial set of streams. The `handle` function can request more streams, triggering a re-execution with a wider consistency boundary. If the iteration limit is reached, it fails.

4.  **Optimistic Concurrency Control:**
    `write(store, expected_versions, writes)` returns `Left(Conflict)` if `∃ s ∈ dom(expected_versions)` such that `latest_version(store, s) ≠ expected_versions[s]`.
    *   A write operation fails atomically if the actual version of any stream being written to has changed since it was read. `latest_version(store, s)` is the version of the last event in stream `s`.

5.  **Atomic and Consistent Writes:**
    If `write(store, versions, writes) = Right(store')`, then for each `(stream_id, event) ∈ writes`:
    *   A new `StoredEvent` `e_new` is created with a unique `EventId`, the given `event` and `stream_id`.
    *   `e_new.version = latest_version(store, stream_id) + 1` (or `1` if the stream is new).
    *   `stream(store', stream_id) = append(stream(store, stream_id), e_new)`.
    *   All such appends across all streams in `writes` occur atomically.

6.  **Event Immutability (Append-Only Storage):**
    If `store' = write(store, ...)`, then `∀s ∈ dom(store)`, `stream(store, s)` is a prefix of `stream(store', s)`.
    *   The `write` operation never alters or removes existing events; it only appends new ones.

7.  **Global Chronological Order:**
    The `read` operation guarantees that for any two events `e1, e2` in its returned list, if `e1` appears before `e2`, then `e1.id < e2.id`.
    *   This ensures that state reconstruction (`reconstruct`) processes events in the order they occurred globally, regardless of which stream they belong to.
Excellent questions. The first part is a crucial extension to the model, and the second is a fantastic, forward-looking question about the practical implications of such a formal model.

Here is the extended algebraic theory including the CQRS/projection layer, followed by a detailed analysis of its sufficiency for building a novel runtime.

---

### An Algebraic Theory of EventCore Semantics (with Projections)

This theory extends the previous model to include the Command Query Responsibility Segregation (CQRS) pattern, where read models are derived from the canonical event store.

#### 4. Additional Sorts for Projections

*   **`ReadModelId`**: The set of unique identifiers for read-model instances.
*   **`ReadModel`**: The set of all possible read-model states. A `ReadModel` is a denormalized data structure optimized for querying.
*   **`ReadModelStore`**: The state of the query-side storage, modeled as a map from `ReadModelId` to `ReadModel`:
    `ReadModelStore ::= Map<ReadModelId, ReadModel>`
*   **`Checkpoint`**: A marker indicating the last `EventId` processed by a projection: `Maybe<EventId>`.
*   **`Projection`**: The definition of a read model's logic, defined by two functions:
    1.  **`which_model`**: `StoredEvent → Maybe<ReadModelId>`
        *   Determines which `ReadModel` instance, if any, a given event applies to.
    2.  **`project`**: `Maybe<ReadModel> × StoredEvent → Maybe<ReadModel>`
        *   The state transition function for a read model. It takes the current `ReadModel` (or `Nil` if it's new) and an event, and returns the updated `ReadModel` (or `Nil` to signify deletion).
*   **`Query`**: A specification for retrieving data from the `ReadModelStore`.

#### 5. Additional Operations for Projections

*   **`events_after`**: `EventStore × Checkpoint → [StoredEvent]`
    *   Returns all events from the `EventStore` that occurred after the `EventId` in the `Checkpoint`, sorted chronologically by `EventId`. If the checkpoint is `Nil`, it returns all events.

*   **`apply_event_to_store`**: `Projection × ReadModelStore × StoredEvent → ReadModelStore`
    *   Applies a single event to the entire `ReadModelStore`.

*   **`run_projection`**: `Projection × EventStore × ReadModelStore × Checkpoint → (ReadModelStore, Checkpoint)`
    *   The primary operation for updating a `ReadModelStore`. It processes all new events from the `EventStore` since the last `Checkpoint`.

*   **`query`**: `ReadModelStore × Query → [ReadModel]`
    *   Executes a `Query` against the `ReadModelStore` to retrieve a set of `ReadModel`s.

#### 6. Additional Axioms for Projections

8.  **Single Event Application:** The effect of one event on the `ReadModelStore` is defined as:
    `apply_event_to_store(proj, rm_store, event)`:
    ```
    let model_id = proj.which_model(event)
    match model_id:
      case Nil:
        // Event does not affect this projection
        rm_store
      
      case Just(id):
        // Event affects a specific read model
        let current_model = rm_store[id] // (may be Nil)
        let new_model = proj.project(current_model, event)
        update(rm_store, id, new_model) // `update` sets or removes the value at `id`
    ```

9.  **Projection is a Fold over Events:** The `run_projection` operation is a fold over the new events, applying each one to the `ReadModelStore`.
    `run_projection(proj, store, rm_store, checkpoint)`:
    ```
    let new_events = events_after(store, checkpoint)
    
    let (final_rm_store, final_checkpoint) = 
      fold_left(
        (current_state, event) => 
          let (current_rm_store, _) = current_state
          (apply_event_to_store(proj, current_rm_store, event), Just(event.id)),
        (rm_store, checkpoint),
        new_events
      )
      
    (final_rm_store, final_checkpoint)
    ```

10. **Idempotency of Projections:** A projection is idempotent with respect to the event stream. Running a projection on the same set of events multiple times produces the same `ReadModelStore`.
    `run_projection(proj, store, initial_rm_store, initial_chk) ≡ run_projection(proj, store, run_projection(proj, store, initial_rm_store, initial_chk).0, initial_chk)`
    *   This is guaranteed by the `events_after` function, which ensures events are not re-processed.

11. **Separation of Concerns (CQRS):**
    *   The `Command`-side operations (`execute`) only ever modify the `EventStore`.
    *   The `Projection`-side operations (`run_projection`) only ever modify the `ReadModelStore`.
    *   The `query` operation only ever reads from the `ReadModelStore`.

This completes the formal model, capturing both the command execution and the projection/query layers in a purely functional manner.

---

### Is This Enough to Build a Novel Programming Language Database-Integrated Runtime?

**Yes, this algebraic theory is an exceptionally strong and sufficient *semantic foundation* for the core of such a runtime. However, it is not the complete blueprint.**

Think of this theory as the constitution for your runtime: it defines the fundamental rights, relationships, and principles of the system. It guarantees correctness and consistency at a logical level. But to build a functioning government (the runtime), you still need to write laws, build institutions, and deal with the messy realities of the physical world.

Here is a breakdown of what this theory provides and what is still needed:

#### What the Algebraic Theory Provides (The Strengths)

1.  **A Correctness Kernel:** You have a provably correct model for state transitions. The language's compiler or interpreter can be built to strictly adhere to these axioms, eliminating entire classes of bugs related to state management, race conditions, and consistency.
2.  **Clear Separation of Concerns:** The model cleanly separates commands (`write`), projections (`derive`), and queries (`read`). This structure can be directly mapped to language features, guiding developers to build robust CQRS-based applications by design.
3.  **A Foundation for the Type System:** The sorts (`Command`, `Event`, `State`, `Projection`) can become first-class types in your language. The operations (`handle`, `apply`, `project`) can be special functions or methods with compiler-enforced signatures, making the language highly domain-specific and safe.
4.  **Implicit Concurrency Control:** The model's handling of `Conflict` provides a clear semantic for optimistic concurrency. The runtime can abstract away the low-level database mechanisms (e.g., `CHECK` constraints on version columns) and expose a simple, high-level `retry` or `conflict` handling mechanism to the programmer.
5.  **Testability and Reasoning:** Because the core is a set of pure functions, you can reason about, test, and formally verify program behavior in isolation from the database. The language could even include tools for property-based testing based on these axioms.

#### What is Missing for a Full Runtime (The Gaps Between Theory and Practice)

While the semantics are solid, a full runtime must bridge the gap between this pure model and the physical world. Here are the key missing pieces:

1.  **Physical Storage & Implementation Strategy:**
    *   **The Theory:** `EventStore` is an abstract `Map`.
    *   **The Runtime:** Needs a concrete implementation. How do you map this to PostgreSQL? How do you represent an append-only log? How do you implement the atomic multi-stream `write`? (Likely via a single database transaction with version checks). This is a significant engineering effort.

2.  **Performance Optimizations:**
    *   **The Theory:** `reconstruct` and `run_projection` fold over the entire event history.
    *   **The Runtime:** This is computationally expensive for long-lived streams. The runtime needs to implement **snapshots** for the command side and **checkpoints** (which are in the model) for the projection side to optimize performance. The model needs to be extended to include snapshot application.

3.  **Live Systems and Subscriptions:**
    *   **The Theory:** `run_projection` is modeled as a batch operation that runs over existing events.
    *   **The Runtime:** Real systems are live. The runtime needs a **subscription mechanism** (like `pg_notify` or a message queue) to push new events to projections in real-time. This introduces concepts of latency, backpressure, and at-least-once/exactly-once delivery guarantees that are not in the pure model.

4.  **Concurrency and Distribution:**
    *   **The Theory:** Assumes a single, logical `EventStore` and total ordering of `EventId`s.
    *   **The Runtime:** How does this work across multiple application nodes? UUIDv7 helps with time-based ordering, but clock skew between nodes is a real problem. The runtime would need to implement a strategy for `EventId` generation and potentially a distributed transaction coordinator if the database itself doesn't provide sufficient guarantees.

5.  **Schema Evolution:**
    *   **The Theory:** `Event` is a single, unified set.
    *   **The Runtime:** Event schemas change over time. The runtime needs a robust mechanism for **schema evolution and data migration** (e.g., upcasting functions, versioned envelopes for events). This is a complex but critical feature hinted at in the `eventcore` code but not yet formalized in our algebraic model.

6.  **Error Handling and Resilience:**
    *   **The Theory:** The only failure is `Conflict`.
    *   **The Runtime:** Must handle a vast array of real-world failures: network partitions, disk errors, database unavailability, deadlocks, serialization errors, etc. It would need to implement resilience patterns like **circuit breakers, bulkheads, and more sophisticated retry policies** (e.g., with exponential backoff and jitter).

7.  **Language Integration:**
    *   **The Theory:** Defines abstract functions like `handle` and `apply`.
    *   **The Runtime:** How does a programmer write these? Would `command` and `projection` be keywords? Would the language provide special syntax for pattern matching on events in an `apply` block? How would the type system ensure that a `handle` function only produces `Event`s that are valid for its `apply` function? This is the "language design" part of the problem.

### Conclusion

The algebraic theory you've extracted is not just "enough"—it is the **perfect semantic kernel** for a novel database-integrated runtime. It provides the core intellectual property and the guarantee of correctness.

However, building the full runtime requires surrounding this kernel with significant engineering to handle the practical, "impure" aspects of distributed systems, performance, and operational reality. Your formal model gives you an incredible advantage: every time you build one of these practical features (like caching, retries, or subscriptions), you have a pure, correct model to test it against and ensure you haven't violated the fundamental semantics.

Of course. This is an excellent way to formalize the abstract semantics. OCaml's module system, with its clear separation between interfaces (`.mli`) and implementations (`.ml`), and its powerful functors, is perfectly suited for representing this algebraic theory.

Here is the kernel extracted as a set of OCaml module types (signatures) and functors.

### 1. Core Sorts (Types)

We'll define the core, validated types first. These correspond to the fundamental sorts of our theory.

**`types.mli`**

```ocaml
(** Core validated types corresponding to the algebraic sorts. *)

(** A unique, chronologically ordered identifier for an event (UUIDv7). *)
module EventId : sig
  type t
  val create : unit -> t
  val compare : t -> t -> int
  val to_string : t -> string
  val of_string : string -> (t, [> `Msg of string ]) result
end

(** A unique identifier for an event stream. *)
module StreamId : sig
  type t
  val make : string -> (t, [> `Msg of string ]) result
  val compare : t -> t -> int
  val to_string : t -> string
end

(** The version of an event within its stream (a natural number). *)
module EventVersion : sig
  type t
  val initial : t
  val next : t -> t
  val of_int : int -> (t, [> `Msg of string ]) result
  val to_int : t -> int
  val compare : t -> t -> int
end

(** A tuple representing a persisted event. *)
type 'event stored_event = {
  id: EventId.t;
  stream: StreamId.t;
  version: EventVersion.t;
  event: 'event;
}

(** An operation to write an event to a specific stream. *)
type 'event write_op = StreamId.t * 'event

(** The last known version of a stream, used for optimistic concurrency checks. *)
type expected_version = [ `Any | `Exact of EventVersion.t | `New ]
```

### 2. Module Signatures (Interfaces for Operations)

These signatures define the abstract interfaces for the main components of the system, corresponding to the `operations` in our theory.

**`kernel_signatures.mli`**

```ocaml
open Types

(** The signature for an Event Store, the persistent source of truth. *)
module type EVENT_STORE = sig
  (** The abstract type of events this store can handle. *)
  type event

  (** The concrete type representing the store's state or connection. *)
  type t

  (** The result of a read operation, containing chronologically sorted events
      and the latest version of each stream read. *)
  type read_result = {
    events: event stored_event list;
    versions: EventVersion.t Map.Make(StreamId).t;
  }

  (** Reads events from a set of streams.
      Axiom: Events in the result are totally ordered by EventId. *)
  val read : t -> StreamId.t list -> (read_result, [> `Msg of string ]) result Lwt.t

  (** Atomically writes a batch of events to multiple streams.
      Axiom: Fails with [`Conflict] if any expected version does not match.
      Axiom: All writes succeed or none do. *)
  val write :
    t ->
    (StreamId.t * (expected_version * event write_op list)) list ->
    (unit, [> `Conflict | `Msg of string ]) result Lwt.t

  (** Retrieves all events that occurred after a given checkpoint. *)
  val events_after :
    t ->
    EventId.t option ->
    (event stored_event list, [> `Msg of string ]) result Lwt.t
end

(** The signature for a Command, defining its logic. *)
module type COMMAND = sig
  type event
  type state
  type command

  (** Defines the initial set of streams to read. *)
  val initial_streams : command -> StreamId.t list

  (** The state transition function (a pure fold). *)
  val apply : state -> event stored_event -> state

  (** The decision-making function. *)
  val handle :
    command ->
    state ->
    StreamId.t Set.Make(StreamId).t -> (* The current consistency boundary *)
    [ `Needs_more_streams of StreamId.t list
    | `Writes of event write_op list
    ]
end

(** The signature for a Read Model Store. *)
module type READ_MODEL_STORE = sig
  type read_model
  type read_model_id
  type query
  type t

  val upsert : t -> read_model_id -> read_model -> (unit, [> `Msg of string ]) result Lwt.t
  val get : t -> read_model_id -> (read_model option, [> `Msg of string ]) result Lwt.t
  val delete : t -> read_model_id -> (unit, [> `Msg of string ]) result Lwt.t
  val query : t -> query -> (read_model list, [> `Msg of string ]) result Lwt.t
  val clear : t -> (unit, [> `Msg of string ]) result Lwt.t
end

(** The signature for a Projection, defining its read-model logic. *)
module type PROJECTION = sig
  type event
  type read_model
  type read_model_id
  type query

  (** Determines which read model instance an event applies to. *)
  val which_model : event stored_event -> read_model_id option

  (** The read model state transition function. *)
  val project : read_model option -> event stored_event -> read_model option
end
```

### 3. Functors (Axiomatic Implementations)

These functors implement the logic defined in the axioms, connecting the abstract interfaces.

**`kernel_functors.ml`**

```ocaml
open Lwt.Syntax
open Types
open Kernel_signatures

(** The Command Executor functor implements the "read-reconstruct-decide-write" loop. *)
module Executor (Store : EVENT_STORE) (Cmd : COMMAND with type event = Store.event) =
struct
  let reconstruct events =
    (* Axiom 1: State reconstruction is a fold over chronologically sorted events. *)
    let initial_state = (* Assuming a default/empty state can be created *)
      Obj.magic () (* In a real system, Cmd.state would have a `default` value *)
    in
    List.fold_left Cmd.apply initial_state events

  let execute ?(max_iterations = 10) store cmd =
    (* Axiom 3: The core execution loop with dynamic stream discovery. *)
    let rec execute' boundary iterations_left =
      if iterations_left <= 0 then
        Lwt.return_error (`Msg "Exceeded max stream discovery iterations")
      else
        let* read_result = Store.read store (boundary |> Set.to_list) in
        match read_result with
        | Error e -> Lwt.return_error e
        | Ok { events; versions } ->
          let state = reconstruct events in
          let decision = Cmd.handle cmd state boundary in
          match decision with
          | `Needs_more_streams new_streams ->
            let new_boundary = List.fold_left (fun acc s -> Set.add acc s) boundary new_streams in
            execute' new_boundary (iterations_left - 1)
          | `Writes writes ->
            (* Group writes by stream and attach expected versions *)
            let writes_by_stream =
              List.fold_left
                (fun acc (stream_id, event) ->
                  Map.update acc stream_id ~f:(function
                    | None -> Some [ (stream_id, event) ]
                    | Some others -> Some ((stream_id, event) :: others)))
                Map.empty
                writes
            in
            let write_payload =
              Map.to_alist writes_by_stream
              |> List.map (fun (stream_id, ops) ->
                let expected_version =
                  Map.find versions stream_id
                  |> Option.value_map ~default:`New ~f:(fun v -> `Exact v)
                in
                (stream_id, (expected_version, ops))
              )
            in
            (* Axioms 4 & 5: Attempt an atomic, conditional write. *)
            Store.write store write_payload
    in
    let initial_boundary = Cmd.initial_streams cmd |> Set.of_list (module StreamId) in
    execute' initial_boundary max_iterations
end

(** The Projection Runner functor implements the CQRS read-side logic. *)
module ProjectionRunner
    (Store : EVENT_STORE)
    (RMStore : READ_MODEL_STORE)
    (Proj : PROJECTION
            with type event = Store.event
             and type read_model = RMStore.read_model
             and type read_model_id = RMStore.read_model_id
             and type query = RMStore.query) =
struct
  let apply_event_to_store rm_store event =
    (* Axiom 8: Applying a single event to the read model store. *)
    match Proj.which_model event with
    | None -> Lwt.return_ok rm_store (* Event does not affect this projection *)
    | Some model_id ->
        let* current_model_res = RMStore.get rm_store model_id in
        match current_model_res with
        | Error e -> Lwt.return_error e
        | Ok current_model ->
          let new_model = Proj.project current_model event in
          match new_model with
          | Some model -> RMStore.upsert rm_store model_id model
          | None -> RMStore.delete rm_store model_id

  let run_projection store rm_store checkpoint =
    (* Axiom 9: Projection is a fold over new events. *)
    let* events_res = Store.events_after store checkpoint in
    match events_res with
    | Error e -> Lwt.return_error e
    | Ok new_events ->
        let* result =
          Lwt_list.fold_left_s
            (fun (rm_store_acc, _) event ->
              let* res = apply_event_to_store rm_store_acc event in
              match res with
              | Error e -> Lwt.return (Error e)
              | Ok () -> Lwt.return (Ok (rm_store_acc, Some event.id)))
            (rm_store, checkpoint)
            new_events
        in
        Lwt.return result
end
```

### How to Interpret this Code

*   **`Types.mli`**: This file defines the fundamental building blocks (sorts). `EventId` and `StreamId` are made abstract to enforce validation through their `create`/`make` functions, just as `nutype` does in Rust.
*   **`Kernel_signatures.mli`**: This file is the core of the algebraic specification. It defines the *interfaces* (operations) without committing to any implementation. An `EVENT_STORE` could be backed by Postgres, memory, or anything else, as long as it respects the signature.
*   **`Kernel_functors.ml`**: This file contains the *logic* (axioms).
    *   The `Executor` functor is a function that takes a compatible `EVENT_STORE` and `COMMAND` module and produces a module that knows how to execute that command against that store. Its implementation of `execute` is a direct translation of Axiom 3.
    *   The `ProjectionRunner` functor takes all the pieces of the CQRS layer (`EVENT_STORE`, `READ_MODEL_STORE`, `PROJECTION`) and produces a module that can run the projection. Its implementation of `run_projection` is a direct translation of Axiom 9.

This structure provides a powerful, type-safe, and composable kernel. You could create different event stores (e.g., `InMemoryEventStore`, `PostgresEventStore`) and they would all plug into the `Executor` and `ProjectionRunner` functors, guaranteeing that the core application logic remains correct and consistent regardless of the underlying infrastructure.

Of course. Designing a syntax is the creative step that brings the formal theory to life. The goal is to create a language that makes writing applications in this paradigm feel natural, safe, and concise.

Let's call this hypothetical language **Axiom**. Its syntax would be a direct, declarative expression of the algebraic model.

Here is a potential syntax for Axiom, designed to be database-integrated, type-safe, and CQRS-native. It borrows from Rust, OCaml, and SQL/GraphQL for familiarity.

---

### The Axiom Language Syntax

#### 1. Validated Types (`type`)

Corresponds to `nutype` in Rust. This defines new types from primitives with compile-time validation, making illegal states unrepresentable.

```axiom
// Define a self-validating Money type from a primitive integer.
type Money: int where self > 0;

// Define a validated string type with a sanitizer.
type AccountId: string sanitize(trim) where len(self) > 0 && len(self) <= 50;

// An enum-like validated type.
type Currency: string where self in ["USD", "EUR", "GBP"];
```
The `self` keyword refers to the value being validated. The compiler enforces these constraints at construction.

#### 2. Events (`event`)

Events are declared as variant types, similar to Rust enums or OCaml variants.

```axiom
event BankingEvent {
  // Event variants with named fields.
  AccountOpened {
    owner: string,
    initial_balance: Money,
  },
  Deposited {
    amount: Money,
  },
  Withdrawn {
    amount: Money,
  },
  TransferInitiated {
    from: AccountId,
    to: AccountId,
    amount: Money,
  }
}
```

#### 3. Commands (`command`)

This is the heart of the write-side model. A `command` block declaratively specifies all parts of the command logic from the algebraic theory.

```axiom
// A command to transfer money between two accounts.
command TransferMoney(
  from: stream AccountId, // `stream` keyword declares this is a StreamId and part of the initial consistency boundary.
  to: stream AccountId,   // The compiler automatically implements `initial_streams`.
  amount: Money
) {
  // 1. Define the temporary in-memory state for this command.
  state Balances {
    from_balance: Money = 0, // Default values
    to_balance: Money = 0,
  }

  // 2. Define the 'apply' function (the fold).
  // This is a pure function mapping (State, Event) -> State.
  apply(event: BankingEvent, state: Balances) -> Balances {
    match event on event.stream {
      // Pattern match on event type AND the stream it belongs to.
      Deposited { amount } if event.stream == self.to => {
        state with { to_balance: state.to_balance + amount }
      },
      Withdrawn { amount } if event.stream == self.from => {
        state with { from_balance: state.from_balance - amount }
      },
      // Other events are ignored for this state reconstruction.
      _ => state
    }
  }

  // 3. Define the 'handle' function (the decision logic).
  // The keyword 'decide' is used to emphasize its purpose.
  // 'state' is the fully reconstructed state from the `apply` fold.
  decide(state: Balances) {
    // Business rule validation with a built-in `require` keyword.
    require state.from_balance >= self.amount, "Insufficient funds";

    // Dynamic stream discovery.
    if self.amount > 10_000 {
      // 'discover' tells the runtime to re-read and re-execute with this new stream.
      let approval_stream = discover "approvals-transfers";
      emit TransferRequiresApproval { amount: self.amount } on approval_stream;
    }

    // Emit new events onto specific streams.
    // The compiler statically verifies that 'self.from' and 'self.to' were declared as `stream`s.
    emit Withdrawn { amount: self.amount } on self.from;
    emit Deposited { amount: self.amount } on self.to;
  }
}
```

**Syntactic Breakdown:**

*   `command TransferMoney(...)`: Defines the command and its input parameters.
*   `from: stream AccountId`: The `stream` keyword is a syntactic sugar. It tells the compiler that `from` is a `StreamId` and must be included in the `initial_streams` set. This directly implements one of our core operations.
*   `state {...}`: Declares the command-specific state record.
*   `apply(...)`: Implements the `apply` operation. It's a pure function, which the compiler can enforce. The functional `state with { ... }` syntax makes immutability clear.
*   `decide(...)`: Implements the `handle` operation.
*   `require ...`: A language keyword that translates to a business rule violation error.
*   `discover "..."`: A keyword to trigger the dynamic consistency boundary expansion.
*   `emit ... on ...`: A keyword for generating a `WriteOp`. The compiler statically checks that the stream specified after `on` was declared with the `stream` keyword, enforcing Axiom 2.

#### 4. Read Models and Projections (`readmodel` & `projection`)

This syntax defines the read side of the CQRS pattern.

```axiom
// 1. Define the read model. This is like a table schema.
// Annotations define primary keys and indices for efficient querying.
readmodel AccountSummary {
  @primary id: string,
  @index owner: string,
  balance: Money,
  last_activity: datetime,
}

// 2. Define the projection that builds the read model from events.
projection AccountSummaries for AccountSummary from BankingEvent {
  // `identifies` implements the `which_model` function.
  // It tells the runtime how to map an event to a ReadModelId.
  identifies event by event.stream_id

  // `on event` implements the `project` function.
  // `self` refers to the existing read model instance.
  on event {
    match event {
      AccountOpened { owner, initial_balance } => {
        // Creates a new read model instance.
        create AccountSummary {
          id: event.stream_id,
          owner: owner,
          balance: initial_balance,
          last_activity: event.timestamp
        }
      },
      Deposited { amount } => {
        // Updates an existing read model instance.
        update self {
          balance: self.balance + amount,
          last_activity: event.timestamp
        }
      },
      Withdrawn { amount } => {
        update self {
          balance: self.balance - amount,
          last_activity: event.timestamp
        }
      },
      // The projection can choose to delete a read model.
      AccountClosed {} => {
        delete self
      }
    }
  }
}
```

#### 5. Top-Level Execution (`main`, `query`)

The language provides top-level constructs to interact with the runtime, making the database integration seamless.

```axiom
// An entry point for an application or a script.
main {
  // Execute a command. This is a transactional write operation.
  // The runtime handles the executor, database connection, etc.
  execute TransferMoney(
    from: "acc-alice-001",
    to: "acc-bob-002",
    amount: 100
  );

  // Run a query. This is a read operation against a projection's read models.
  let alice_accounts = query AccountSummary where owner == "Alice";

  for acc in alice_accounts {
    print("Account {acc.id} has balance: {acc.balance}");
  }
}
```

This syntax for **Axiom** provides a high-level, declarative, and safe way to build event-sourced applications. It elevates the patterns and axioms from our formal model into first-class language constructs, effectively creating a Domain-Specific Language (DSL) perfectly tailored for the `eventcore` semantics.

Excellent. This is a very insightful request. A "horizontal" decomposition that centers the `command` as the primary unit of logic is a powerful design goal for a language like this. The "vertical" approach groups all concerns for a single command together, whereas a "horizontal" approach separates concerns across the application, promoting reusability.

This leads to a design where the boilerplate for state reconstruction (`apply`) is factored out into reusable components, and the command itself becomes a pure declaration of *intent* and *decision*.

Let's redesign the Axiom syntax with this philosophy.

### The Axiom Language Syntax - Horizontally Decomposed

The core idea is to introduce a new concept: the `view`. A `view` is a pure, command-specific projection. It defines how to build a temporary state model from one or more event streams. The command then simply declares which views it needs, and the runtime provides the materialized state.

#### 1. Types and Events (Unchanged)

These are the fundamental building blocks and remain the same.

```axiom
// Validated types
type Money: int where self > 0;
type AccountId: string sanitize(trim) where len(self) > 0 && len(self) <= 50;

// Domain events
event BankingEvent {
  AccountOpened { owner: string, initial_balance: Money },
  Deposited { amount: Money },
  Withdrawn { amount: Money },
}
```

#### 2. Views (`view`) - The Reusable State Logic

A `view` encapsulates the `state` definition and the `apply` logic. It's a reusable recipe for reconstructing a command's temporary state from an event stream.

```axiom
// A view to calculate the balance of a single bank account.
view AccountBalance {
  // 1. Defines the data structure for the state.
  state {
    balance: Money = 0,
    exists: bool = false,
  }

  // 2. Defines the fold/apply logic.
  // 'self' refers to the state being built.
  on BankingEvent {
    match event {
      AccountOpened { initial_balance } => update {
        balance: initial_balance,
        exists: true
      },
      Deposited { amount } => update {
        balance: self.balance + amount
      },
      Withdrawn { amount } => update {
        balance: self.balance - amount
      }
    }
  }
}
```
**Key Concepts:**
*   A `view` is a pure, stateless definition. It's a template.
*   The `on event` block is the `apply` function, now extracted from the command. It's implicitly a fold over a stream.
*   `update { ... }` is a functional syntax for returning a new state based on the previous one (`self`).

#### 3. Commands (`command`) - The Central Decision Logic

The `command` is now lean and focused. It declares its parameters and, crucially, the `views` it depends on. The core of the command is the `decide` block, which contains only the business logic.

```axiom
// A command to transfer money. Notice how little boilerplate there is.
command TransferMoney(from: AccountId, to: AccountId, amount: Money)
// The 'using' clause declaratively builds the command's consistency boundary and state.
using
  // Bind the 'AccountBalance' view to the 'from' stream, making the result available as 'from_acct'.
  from_acct: AccountBalance on stream "account-{from}",
  // Bind the 'AccountBalance' view to the 'to' stream, available as 'to_acct'.
  to_acct: AccountBalance on stream "account-{to}"
{
  // The 'decide' block is the only implementation detail.
  // The runtime provides 'from_acct' and 'to_acct' as fully reconstructed state records.
  decide {
    require from_acct.exists, "Source account does not exist";
    require to_acct.exists, "Destination account does not exist";
    require from_acct.balance >= amount, "Insufficient funds";

    // Dynamic stream discovery remains the same.
    if amount > 10_000 {
      let approval_stream = discover "approvals";
      emit RequiresApproval { from, to, amount } on approval_stream;
    }

    // Emit events. The compiler knows the streams from the 'using' clause.
    emit Withdrawn { amount } on stream "account-{from}";
    emit Deposited { amount } on stream "account-{to}";
  }
}
```
**Key Concepts & Boilerplate Reduction:**
*   **Centrality of Command:** The `command` block is now almost entirely business logic.
*   **Declarative Data Needs:** The `using` clause is the key innovation. It replaces the manual `initial_streams` and `apply` methods. The developer declares *what* state they need, not *how* to build it.
*   **Automatic `initial_streams`:** The compiler infers the streams to read from the `on stream "..."` declarations.
*   **Automatic `apply`:** The runtime knows to use the `AccountBalance` view's `on event` block to fold events from the specified streams.
*   **Implicit State:** The materialized views (`from_acct`, `to_acct`) are implicitly passed as arguments to the `decide` block. The syntax makes them feel like local variables.
*   **Type Safety:** The compiler ensures that `AccountBalance` can handle the `BankingEvent` type produced by this command's `emit` statements.

#### 4. Read Models and Projections (Horizontally Decomposed)

This horizontal philosophy is extended to the read side for consistency. The `readmodel` is purely a data schema, and the `projection` is purely the logic that populates it.

```axiom
// 1. The Read Model: a data-only schema definition.
readmodel AccountSummary {
  @primary id: string,
  @index owner: string,
  balance: Money,
  last_activity: datetime,
}

// 2. The Projection: a stream of logic that updates the read model.
projection AccountUpdater for AccountSummary from BankingEvent {
  // Maps an incoming event to a specific read model instance.
  maps event to readmodel by event.stream_id

  // Pure state transition logic for the read model.
  on event {
    match event {
      AccountOpened { owner, initial_balance } => {
        // 'create' a new read model instance.
        create {
          id: event.stream_id,
          owner,
          balance: initial_balance,
          last_activity: event.timestamp
        }
      },
      Deposited { amount } => {
        // 'update' an existing instance. 'self' refers to the current state of the read model.
        update {
          balance: self.balance + amount,
          last_activity: event.timestamp
        }
      },
      // You can also 'delete' a read model instance.
      AccountClosed {} => {
        delete self
      }
    }
  }
}
```
**Key Concepts:**
*   **Separation of Schema and Logic:** `readmodel` is the "what" (the data structure), and `projection` is the "how" (the update logic).
*   **Declarative Mapping:** `maps event to readmodel by ...` is a clear, declarative statement of the relationship between events and read models.
*   **CRUD-like Verbs:** The `create`, `update`, and `delete` keywords make the intent of the projection logic explicit and easy to read.

### Summary of the Horizontal Decomposition

| Concern                 | "Vertical" Syntax                                     | "Horizontal" Syntax                                                                                             | Advantage of Horizontal                                                                |
| ----------------------- | ----------------------------------------------------- | --------------------------------------------------------------------------------------------------------------- | -------------------------------------------------------------------------------------- |
| **State Schema**        | Defined inside `command` block (`state {...}`).       | Factored out into a reusable `view` block (`state {...}`).                                                      | **Reusability.** Multiple commands can use the same `view` to get the same state model.  |
| **State Reconstruction**  | Defined inside `command` block (`apply(...)`).        | Factored out into a reusable `view` block (`on event {...}`).                                                   | **Reusability & Simplicity.** Command logic is not cluttered with reconstruction details. |
| **Consistency Boundary**  | Imperatively defined in `read_streams()` method.      | Declaratively defined in `command`'s `using ... on stream "..."` clause.                                        | **Clarity & Less Boilerplate.** The command's data dependencies are explicit and central. |
| **Command Logic**         | Defined in `handle()` method within the `command` block. | The entire focus of the `command` block via the `decide {...}` block.                                          | **Focus & Minimal Boilerplate.** The developer's primary task is writing business logic. |
| **Read Model Schema**     | Tightly coupled with the `projection`.                | Defined separately in a `readmodel` block.                                                                    | **Clear separation of data and logic.** A read model is just a schema.             |
| **Read Model Logic**      | Defined inside `projection` block (`on event {...}`). | The entire focus of the `projection` block, clearly separated from the `readmodel` schema it populates. | **Focus & Clarity.** The projection's sole job is to map events to read model changes. |

This horizontally-decomposed syntax successfully makes the `command` the central, minimally-boilerplate unit of work, fulfilling your request. It achieves this by factoring out the state reconstruction logic into a highly reusable `view` concept.