AREST Developer Docs

Self-contained reference for building on arest. FORML 2 readings compile to a database schema, constraint rules, state machines, and a REST API with HATEOAS, all from one β-reducer over Backus's FFP algebra.

View the Project on GitHub graphdl/arest

10 · Self-Modification

One of the load-bearing claims of AREST is that the system can change its own schema without leaving the algebra. There are two paths: immediate self-modification via compile, and governed self-modification via propose. Both preserve all five theorems (Corollary 5: Closure Under Self-Modification).

The compile path

compile takes reading text, parses it, compiles it, and merges the resulting defs into DEFS via the store operator ↓DEFS. Subsequent SYSTEM applications evaluate the new definitions as if they had been there from the start.

# CLI
arest-cli readings/ --db app.db        # initial compile
arest-cli readings/v2/ --db app.db     # re-compile with new readings

# MCP
compile({ readings: "New Fact Type: User has Loyalty Tier.\n  Each User has at most one Loyalty Tier." })

compile is the raw mechanism. Use it when:

Because compile reaches DEFS directly, it bypasses any approval gate. Anyone with the ability to call compile can change your schema. In multi-tenant deployments, gate compile behind an admin role.

The propose path

propose creates a Domain Change entity with the proposed readings, nouns, or constraints, then enters the state machine declared in the bundled evolution.md:

Proposed → Under Review → Approved → Applied
         ↘ Rejected
         ↘ (back to Proposed via Revise)

The Domain Change entity carries:

propose({
  rationale: "Add loyalty tier tracking",
  target_domain: "orders",
  readings: ["Customer has Loyalty Tier.\n  Each Customer has at most one Loyalty Tier."],
  nouns: ["Loyalty Tier"]
})
// → { change_id: "dc-lx9f4", status: "Proposed", next_actions: [...] }

Then transitions:

transition({ noun: "Domain Change", id: "dc-lx9f4", event: "review" })          // → Under Review
transition({ noun: "Domain Change", id: "dc-lx9f4", event: "approve-change" })  // → Approved
transition({ noun: "Domain Change", id: "dc-lx9f4", event: "apply" })           // → Applied

On apply, the engine runs compile on the proposed readings, which means the change actually takes effect only when the state machine reaches Applied. Between Proposed and Applied, the proposed elements exist only as data on the Domain Change entity, and they are not yet in DEFS.

Human gates

The metamodel declares deontic constraints that require human review for certain domains:

It is forbidden that a Domain Change targeting Domain 'evolution' is applied without Signal Source 'Human'.
It is forbidden that a Domain Change targeting Domain 'organizations' is applied without Signal Source 'Human'.
It is forbidden that a Domain Change targeting Domain 'core' is applied without Signal Source 'Human'.

Changes to the metamodel itself (core, evolution, organizations) cannot be applied unless a Human signal source is attached. An autonomous agent proposing a metamodel change gets a deontic violation, and the change stays in the Approved state while it waits for human sign-off.

You can extend this pattern to your own domains:

It is forbidden that a Domain Change targeting Domain 'billing' is applied without Signal Source 'Human'.

Signals

A Domain Change is typically triggered by a Signal:

Signal(.Signal Id) is an entity type.

Signal has Signal Source.
Signal leads to Domain Change.

Signal sources: Constraint Violation, Human, Error Pattern, Feature Request, Support Request. The LLM validate verb (see MCP verbs) naturally produces Constraint Violation signals; a customer support integration might produce Support Request signals.

Preserving the theorems

Corollary: Closure says all five theorems hold after self-modification:

  1. Grammar Unambiguity depends on the grammar itself, not on D. Unaffected.
  2. Specification Equivalence depends on parse and compile being injective stateless functions. Unaffected.
  3. Completeness of State Transfer operates over P and S, both of which now include the new content. Still holds.
  4. HATEOAS as Projection operates over P and S. Still holds.
  5. Derivability holds because every value in the representation is a ρ-application, regardless of when the definitions entered DEFS.

The Curry-Howard correspondence applies: proposing a new fact type is proposing a theorem. CSDP validation is the proof check. Successful ingestion is the proof. The system can only evolve by proving something new.

Auditability

Every Domain Change is itself an entity in P. Every status transition is a state-machine event in the audit log. Every applied change leaves a trail:

The same derivation chain that shows why a User accesses a Domain also shows how the schema that made that access possible came to exist. The system is self-documenting by construction.

What’s next

This is the last doc. You have:

The next logical step is to build something real. The tutor subfolder ships a sample app and three progressive lesson tracks (easy, medium, and hard) that exercise every feature end to end. If you run into something these docs do not answer, open an issue, since the docs are meant to be self-contained.