Argon RFDs
Design decision records for the Argon language, runtime, and toolchain.
An RFD records why a choice was made. It is not the specification. The Lean 4 mechanization at spec/lean/ is canonical for the substrate; the reference manual (Part I of this book) describes the surface in prose. RFDs explain how those landed where they did.
Format
- Filename:
NNNN-kebab-case-name.md. Four-digit, no reuse. Numbers are not recycled even when an allocation is abandoned, so the sequence may carry gaps: 0012 was never authored — the number was skipped during a period of concurrent branch allocation (the same churn that renumbered the refinement RFD 0016 → 0017 once numeric-tower took 0016 onmain) and the slot was left empty rather than reused. - Structure: Question · Context · Decision · Rationale · Alternatives · Consequences · Open questions.
- States:
discussion— open; not committed.committed— decided and binding. Implementation may or may not have landed; the decision is fixed.accepted — partially implemented— decided and binding, with implementation landed in part; theState:line annotates what has shipped and what remains.superseded— replaced by a later RFD. Cite the successor.
Authoring an RFD
RFDs live at spec/rfd/ in the repository. The published book reflects whatever is on main. To open a new RFD, allocate the next number, write the file, and submit it via PR — discussion happens on the PR or in linked threads, not by gating merge on consensus.
The format mirrors Oxide Computer Company’s RFD process (Yegge / Dijkstra-via-Bryan-Cantrill lineage) but lighter: no separate authoring tool, no review-state tracker, no required pre-commit lint. A repository PR is the discussion vehicle; the RFD’s State: field carries the decision status.
Index
| # | Title | State |
|---|---|---|
| 0001 | ID architecture | discussion |
| 0002 | #[comptime] attribute | discussion |
| 0003 | Reasoner backend dispatch | discussion |
| 0004 | pub fact declarations | discussion |
| 0005 | Relation subsumption | committed |
| 0006 | Field mutability via mut | discussion |
| 0007 | Missing-value semantics under OWA | discussion |
| 0008 | Standpoint-sheaf equivalence proof roadmap | committed (Path A landed) |
| 0009 | std::mlt library scope | discussion |
| 0010 | Negative facts / strong negation | discussion |
| 0011 | Aggregate semantics under OWA | discussion |
| 0013 | Toolchain distribution | accepted — partially implemented |
| 0014 | Runtime serving surface | discussion |
| 0015 | mutate body surface: EdgeQL-shaped, set-semantic | committed |
| 0016 | Numeric tower: exact by default | committed |
| 0017 | Refinement classification: where (primitive) vs iff (defined) | committed |
| 0018 | Production reasoner: the incremental DBSP engine | accepted — partially implemented |
| 0019 | Mutation write-path correctness: construction, identity, read-your-writes, exact values | accepted — partially implemented |
| 0020 | The runtime data engine: a composable query + reasoning pipeline | accepted — partially implemented |
| 0021 | The reasoner execution engine (as built): joins, optimizer, factorization, BYODS, incrementality discipline | committed |
| 0022 | Package-path addressing (pkg, not crate) and the build evaluability gate | committed |
| 0023 | Reflective TypeRef: type-as-value in the meta-calculus (RP-003 GAP-1) | committed |
| 0024 | Allen interval algebra as a library (std::allen), not substrate operators | committed |
| 0025 | check discharge: vocabulary-staged compile-time and runtime constraint checking | accepted |
| 0026 | Trait rule members: clause-union dispatch, conformance, and the implements intrinsic | accepted — implementation planned |
| 0027 | The meta-property plane: axis bindings, catalog tiers, value-position resolution, and substrate-neutral modifiers | accepted — implementation planned |
| 0028 | Defeasibility redesign: honest heads, the defeat-directive plane, and strategy as a compilation scheme | accepted — implementation planned |
| 0029 | Derived values and aggregate terms: body-level binding, aggregate sources, rounding | committed |
| 0030 | Package dependencies ([dependencies], path deps v1) | committed |
| 0031 | The relation-constraint plane + meta-property completion | committed |
| 0032 | oxup manages editor-extension installation | committed |
| 0033 | The ad-hoc query and mutation surface | accepted — implemented |
| 0034 | Source text encoding and the Unicode lexical policy (UAX #31 identifiers, NFC, module reachability) | committed |
| 0035 | The composable operator-tree execution pipeline: shared LogicalPlan lowering, tree optimizer, physical mapper, generalized executor, table operators | discussion |
| 0036 | Heterogeneous and specialized data stores: foreign federation, external-valued attributes, persistence swap; the connector SPI, placement, world-assumption tiering | discussion |
| 0037 | The macro atom: a phase-separated, hygienic, declarative-first expander over surface syntax | discussion |
| 0038 | The prelude, ambient scope, and symbol-precise stdlib loading | discussion |
| 0039 | Composable mutations: nested invocation and derived reads | accepted — implemented |
| 0040 | The procedural macro layer: a total, structurally-recursive meta-language over reflected syntax | discussion |
| 0042 | The re-checkable emission boundary: a self-validating .oxbin and sound direct artifact emission | discussion |
| 0043 | Theory packages and the neutrality boundary: where ontologies and higher-order theories live | discussion |
| 0044 | Package registry, workspaces, and distribution: a static content-addressed registry over the CDN | discussion |
| 0045 | The world-assumption write-side: refuse-on-K3-not and the #[world] per-concept opt-in | discussion |
| 0046 | Derivation serving surfaces: query, delta, explain, trace (kill the per-rule derive loop) | discussion |
| 0047 | The temporal value library (TC39-Temporal-modeled std) and the value/ontology boundary | discussion |
| 0048 | The test atom: in-language unit tests, and why a test is substrate | accepted — partially implemented |
| 0049 | Error-tolerant diagnostics: recovery, source-faithful expansion, What/Where/Why/Fix | discussion |
| 0050 | Documentation architecture: three books, correctness by construction, and a verified authoring pipeline | discussion |
| 0051 | oxfmt: a canonical, idempotent source formatter over the shared CST | discussion |