Phase 0: Foundation — Index
The formal core calculus for an AI-native programming language. Five sections; written in spec-style (precise, prescriptive, with rationale) rather than the survey-style of the original design memos.
Phase 0 produces the contract that the rest of the project builds against. A full end-to-end compiler through LLVM and the Phase 1 runtime stack is Phase 1 work; a partial reference implementation may exist earlier for engineering feedback (see Section 2 §19 and decisions/phase-0-reference-implementation-status.md).
The sections
Type System Foundation — grammar of types, refinement language (Presburger arithmetic via Z3), type formation, compile-time/runtime phase distinction.
Core Operation Set & Typing Rules — ten core operations (unary, cast, binary, matmul, reduce, transpose, reshape, broadcast, slice, concat). Reduce has two typing rules—standard reduction and keepdims (
reduce-keep)—as one IR operation with a mode flag. Commits to no implicit broadcasting and the controlled unsoundness of reshape's volume axiom.Subtyping and Coercion — refinement-only subtyping; dtype/shape/rank invariant; explicit coercions for everything else. Bidirectional type-checking as the algorithmic strategy.
Operational Semantics — tensors as functions from index tuples; small-step reduction with a heap; type soundness theorem statements (proofs deferred to Phase 6); the principled separation of structural and numerical correctness.
Implementation Infrastructure — OCaml + Rust + Lean 4; MLIR via textual emission; Z3 via OCaml bindings; repository layout; build orchestration; Phase 0 exit criteria.
Key commitments
The decisions that shape everything downstream:
| Decision | Section |
|---|---|
| Refinement language is quantifier-free Presburger arithmetic, discharged by Z3 | 1, §3 |
| Rank polymorphism rejected for Phase 0 | 1, §5 |
Implicit α ≥ 1 at shape variable introduction |
2, §15 |
| No implicit broadcasting in core IR | 2, §11 |
| Reshape's volume equality is asserted axiomatically (controlled unsoundness) | 2, §10 |
| No implicit dtype promotion | 3, §9 |
| Subtyping affects only the refinement axis; everything else requires explicit coercion | 3, §2 |
| Bidirectional type-checking | 3, §7 |
| Operational semantics is real-valued; FP semantics is a separate Phase 6 concern | 4, §6 |
| Three-language polyglot: OCaml + Rust + Lean 4 | 5, §2 |
| MLIR access via textual emission, not C++ API | 5, §3 |
What Phase 0 does not include
- Effects (mutation, randomness, async memory). Phase 2.
- Sharding / distribution. Phase 3.
- Sparsity / structured tensors. Phase 4.
- Hardware capabilities. Phase 5.
- Verified compilation passes. Phase 6 (parallel track).
- Surface syntax. Phase 7.
- Working compiler. Phase 1.
Phase 0 is the foundation. Each later phase extends one of the refinement axes or adds machinery, and each one's design rests on the contract Phase 0 establishes.
Suggested reading order
For a first pass: read in numerical order, 1 → 2 → 3 → 4 → 5. The dependencies are sequential.
For a quick sense of the framework: Section 1 §2 (grammar), Section 2 §17 (decisions table), Section 4 §6 (the numerical-semantics gap), Section 5 §9 (exit criteria). Maybe 30 minutes.
For the implementation plan specifically: Section 5 alone, then come back for the typing rules in Sections 1–3 when the build is underway.
Phase 0 exit criteria
Section 5 §9 lists seven criteria. Six are objective (specs exist, repo skeleton, compiler and runtime validation, Lean builds, and CI or a documented local test gate when hosted CI is deferred — see REVIEW-CHECKLIST.md §4). The seventh — "the author is willing to commit to Phase 1" — is judgment, not metric. Phase 0 is the place to discover the framework is wrong; if the foundation feels wrong at the end, revise rather than continue.
For a systematic coverage pass (open issues, previews, exit criteria vs repo, suggested work order), see REVIEW-CHECKLIST.md. A second-reader-style audit log (2026-05-09) lives in second-reader-pass-2026-05-09.md.
Related documents
The strict spec lives here. Companions and forward-looking commitments live in sibling directories:
../companions/— walkthroughs and examples (Phase 0 primitives, real-world LLM/AI patterns with PyTorch comparisons). Open alongside the spec sections for grounding.../forward-tracks/— design commitments that extend Phase 0 without modifying it: CUDA as a first-class concern, RAPIDS-inspired ecosystem architecture, Apache Arrow + typed dataframes as a future research track, bootstrap/self-modeling, and surface design for multiple personas.
The forward tracks are not part of the strict spec but they impose constraints on Phase 1's implementation. If you're moving toward implementation, read both.
What's next
If Phase 0 is accepted: Phase 1 begins. Roughly 4–6 months of part-time work to grow the OCaml compiler stub into a working shape-typed compiler that produces LLVM and runs through the Rust runtime. Phase 1 has its own milestone document, written as the first work item of Phase 1.
If Phase 0 surfaces design issues: revise the affected sections; re-evaluate. The cost is bounded — the normative corpus is cheap to revise; reference code may need coordinated updates (see §02 §19).
If the project is paused or abandoned: the Phase 0 documents stand as a research artifact regardless. The framework itself is the contribution; whether it gets built is a separate decision.