Kina.ai

Specification

Implementation Roadmap: From Design Memos to Working Language

Companion to the AI-Native Programming Language Design Space Series. This is the answer to "if I were going to actually build this, where would I start, and in what order?"

0. Framing first

The design memos lay out a research program. This document is the implementation plan for that program — what to build, in what order, with what deliverables at each step.

A few honest framings before the phases:

This is a 3–5 year research program if done seriously, and most language projects of this scope fail. The graveyard is full of ambitious systems languages with great ideas and no users. The goal of the phasing below is not to ship a production language; it is to produce durable research artifacts at every step — formal calculi, prototypes, papers, verified passes — so that the project has value even if it never reaches a final language.

This is not a from-scratch build. Every phase leans heavily on existing infrastructure: MLIR for the IR substrate, LLVM for code generation, Coq or Lean for verification, Triton or CUTLASS as kernel-level reference, NCCL for collectives. The contribution is the typed framework connecting these pieces, not new versions of any of them.

The right starting question is not "which phase first?" but "which phase is unavoidable?" Phase 0 (the formal core calculus) is unavoidable — you cannot prototype anything without writing down what the type system means. After that, the sequencing becomes a real choice.

A recommendation up front, before the details: start with Phase 0 + a narrow Phase 1 (shapes only, single-target lowering). Get one end-to-end thread working before adding axes. The temptation will be to design the full five-axis type system on paper before implementing anything; resist it. The first refinement axis will reveal design issues the others would have hit too, and fixing them in code is cheaper than fixing them in a paper.

1. Phase 0: Foundation (unavoidable)

Duration: 2–3 months part-time. Output: A formal core calculus, a project skeleton, and a written-down plan for the next two phases.

Goals

Why this is unavoidable

You cannot write a type-checker without a typing judgment. You cannot write a refinement system without choosing a refinement language. You cannot decide whether refinement-typed tensors are the right framework without seeing the typing rules on paper. Every sub-question in the next five phases reduces to "how does this interact with the core typing judgment?" — a question that has no answer until the judgment exists.

This phase has the highest research-leverage-per-hour of the entire program. A well-designed core calculus reveals issues that a quick prototype would hit only at phase 4. A poorly-designed one means rewriting the IR three times.

What I'd recommend you write down

Antonette-specific notes

This is the part of the project most aligned with your existing OCaml DSL work for the flight sim. The core calculus is structurally similar to a typed AST for .aero files: a small typed core, a parser, an elaboration pass, and an emitter. The skill transfers directly.

The choice of mechanization tool deserves thought: Coq for maximum ecosystem (CompCert, MathComp), Lean 4 for better programming integration and a more modern tooling story, F* if you want SMT-augmented verification from the start. Given your verification background, Lean 4 is probably the right answer — newest, most actively developing, and the ML library ecosystem (mathlib, recent Lean 4 ML papers) is growing fast.

2. Phase 1: Shape-typed core (the first shippable thing)

Duration: 4–6 months part-time. Output: A working type-checker for refinement-typed tensors, an MLIR-based lowering to LLVM, and a test suite of small programs (matmul, MLP forward pass, basic activation functions).

Goals

Why this thread first

Shapes are the simplest of the five refinement axes — purely structural, no side effects, no distribution, no hardware concerns. Getting shapes working end-to-end validates:

  1. The IR data structures hold up under real programs.
  2. The type-checker actually catches errors users care about.
  3. The MLIR lowering pipeline works for non-trivial code.
  4. The repository structure scales to multiple passes.

If the framework can't handle shapes cleanly, it won't handle anything else. If it can, the rest of the phases are extensions of the same architecture.

Shippable artifact

A toy compiler that takes a small program in your chosen surface syntax (probably an S-expression IR at first; the real surface language is Phase 7), type-checks it against shape refinements, and produces a runnable LLVM IR file. A repository link, a tutorial, and a short paper — "A Refinement-Typed Tensor Algebra with MLIR Lowering" or similar — is the first publishable artifact.

Risks

The hardest part is symbolic shape arithmetic. Tensor[f32, [B, S, D]] @ Tensor[f32, [B, D, V]] -> Tensor[f32, [B, S, V]] requires the type-checker to verify dimension equality, which means an SMT solver call per operation. Pick a Z3 binding (e.g., z3-sys for Rust) and design for SMT timeouts from day one. PyTorch 2's symbolic shape engine is the closest reference.

3. Phase 2: AD as an effect (the framework test)

Duration: 4–6 months part-time. Output: Effect-handler infrastructure, reverse-mode AD as a handler, numerical-equivalence tests against PyTorch/JAX.

Goals

Why this is the framework test

Memo 2's central claim — that AD and effects share the CPS implementation strategy, and that effects are the unifying abstraction — is testable here. If reverse-mode AD as a handler works, the framework holds. If it doesn't, the framework needs reworking.

This phase also produces the first piece of genuinely new theoretical work in the project: verified AD over a typed effect calculus. Brunel/Mazza/Pagani and Krawiec et al. have the typed-AD foundations; nobody has done it for effect handlers. A POPL-shaped paper is plausible at the end of this phase.

What "works" looks like

Antonette-specific notes

This is the phase where your OCaml 5 awareness or interest pays off. OCaml 5's effect handlers are the most mature production implementation; reading the Sivaramakrishnan et al. PLDI 2021 paper before this phase is high-value. The implementation patterns transfer directly to whatever you build in Rust.

If you want to do the verified-AD-over-effects paper, this is when the proof work starts. The Coq/Lean formalization can run in parallel with the implementation; the proof informs the implementation, the implementation reveals what's actually proof-relevant.

4. Phase 3: Sharding (the distribution axis)

Duration: 6–9 months part-time. Output: Mesh-as-kind, sharding refinements, GSPMD-style propagation, a multi-device runtime.

Goals

Why this is the second-most tractable target

Memo 5 §6 made the case: verified sharding propagation is the most underexploited tractable target in the design space. This phase produces the unverified version; verified version comes in Phase 6. But even the unverified version has research value — GSPMD's rules have not been written down as a formal type system, and doing so is itself a contribution.

The runtime work is non-trivial. A simulator (run all "devices" in one process with explicit synchronization) is the right starting point. Real distributed runtime requires NCCL/Gloo bindings and careful engineering, but is mostly orthogonal to the type-system work.

Shippable artifacts

Antonette-specific notes

The sharding-as-type formalism connects to TerranoxOS capability work conceptually: a sharding spec is a kind of capability over a mesh axis, and resharding is a capability transfer. This is not a deep correspondence — capabilities are about authorization, shardings are about data distribution — but the type-system machinery (refinement types parameterized by a mesh kind) is structurally similar to capability-typed tensors over a mesh of devices.

The kernel-libs error code discipline applies here too: collective failures, mesh-mismatch errors, and sharding-conflict errors all want the gap-based error scheme you've already designed.

5. Phase 4: Sparsity and structure

Duration: 6 months part-time. Output: Refinement types for sparsity patterns, TACO-style format generation, MoE routing as a language construct.

Goals

Why this phase comes here

Sparsity needs the previous three phases as substrate. You need shapes (sparse tensors still have shapes), AD (sparse gradients exist), and sharding (sparse tensors are sharded too) before you can meaningfully add a sparsity refinement. Doing sparsity earlier means re-doing the type system when the other axes arrive.

The MoE routing construct is the biggest design opportunity in this phase. MegaBlocks proved the kernel-level feasibility; nobody has built it as a language construct. A route x to experts where router(x) syntax that lowers to block-sparse matmul is publishable on its own.

Risk

Sparsity composition is the hardest type-system design problem in the whole framework. The "widen unless proven otherwise" rule needs careful design — when does the user get to prove preservation, what's the proof obligation, how does it integrate with the rest of the type-checker? The design memos sketched the answer; the implementation will reveal cases the sketch missed.

6. Phase 5: Hardware capability typing

Duration: 9–12 months part-time. Output: Capability type system, tile-level IR, lowering for one or two hardware targets.

Goals

Why this is the largest phase

Hardware abstraction is where the rubber meets the road. The previous phases are mostly about getting the type system right; this phase is about the type system actually delivering performance. The first hardware target will reveal everything wrong with the IR design — operations that don't lower cleanly, refinements that don't carry the right information, missing primitives.

This is also the phase most likely to require redesign of earlier work. If the capability type system needs information that earlier phases didn't carry in the type, you go back and add it. Plan for this: don't treat earlier phases as frozen.

Shippable artifacts

7. Phase 6: Verification (parallel track, not sequential)

Duration: Ongoing from Phase 2 onward. Output: Mechanized formal calculus (Coq or Lean), verified subsets of key passes (AD, sharding), translation validation infrastructure.

Goals

This phase is not sequential — verification work runs in parallel with implementation from Phase 2 onward. The structure:

Why parallel rather than sequential

Verification at the end of a project means rewriting everything. Verification interleaved with implementation means the implementation is designed for verifiability from the start — refinement-friendly invariants, no hidden mutation, explicit effect tracking. The cost is real but bounded; the payoff is much higher than retrofitting.

Antonette-specific notes

This is the track most directly aligned with your existing work. Frama-C Bronze proofs, the eBPF verifier, the verify-core trait architecture — these are the right precedents. The Lean 4 / Coq learning curve is the main investment; the methodology is something you already have.

The most concrete deliverable: a verified sharding propagation pass. Memo 5 §6 made the case for tractability. Six months to a year of focused work, POPL or PLDI publishable. This single paper would establish the project's verification credentials in the formal-methods community.

8. Phase 7: Surface language and ergonomics

Duration: 6–12 months part-time. Output: A real surface syntax, a type-inference engine, error messages, basic tooling.

Goals

Why this comes near the end

The surface syntax is the easiest thing to change and the hardest thing to commit to. Doing it last means it benefits from all the design lessons of earlier phases. Doing it first means committing to syntax decisions before knowing what the language really needs.

The bias in research languages is to build the surface first because that's what users see. Resist this bias: the surface is a UX layer over the typed IR, and getting the IR right is more important. CompCert, GHC, and SBCL all spent years on their cores before getting reasonable surfaces.

When to skip this

If the goal is "a research artifact that demonstrates the framework," Phase 7 is optional. The compiler can take an S-expression IR forever and still produce papers. Phase 7 is what turns a research artifact into a usable language, which is a separate decision.

9. Sequencing and dependency graph

Phase 0 (foundation) ──┬── Phase 1 (shapes) ──┬── Phase 2 (AD effects) ──┬── Phase 3 (sharding)
                       │                      │                         │
                       │                      │                         ├── Phase 4 (sparsity)
                       │                      │                         │
                       │                      └─── Phase 6 (verification, parallel) ─────────────
                       │                                                                          │
                       └─── Phase 5 (hardware capability) ── Phase 7 (surface lang) ──────────────┘

The forward dependencies:

The realistic critical path is 0 → 1 → 2 → 3 → 5 → 7, with 4 and 6 running in parallel where capacity allows.

10. Realistic timeline

A part-time research project (10–15 hours/week, sustainable):

Year Phases active Milestones
Year 1 0, 1 (completed), 2 (planning) Core calculus written; shape-typed compiler producing correct LLVM for small programs
Year 2 2, start of 3 AD-as-effect working; sharding type system designed
Year 3 3, 4, 6 (start) Sharding inference working; sparsity refinements; first verification artifact
Year 4 5, 6 (continued) Hardware capability typing; first GPU kernel from the language; verified sharding paper
Year 5+ 7, 6 (continued), production hardening Surface language; tooling; community

Full-time would compress this by roughly 2x. Adding collaborators is mostly irrelevant in early phases (small team, deep design work) and increasingly useful from Phase 5 onward (parallel hardware backends, runtime engineering, surface-language tooling).

11. The "weekend prototype" version

If the question is "what would I build this weekend to convince myself the framework is real?", a much smaller version exists:

That's a weekend or two, no more. It's the smallest thing that demonstrates "yes, refinement-typed tensors work as a research idea." Whether to extend it into the full Phase 0 + 1 work is a separate decision, and one worth deferring until after the prototype reveals what the design really wants to be.

12. Risks and abandonment criteria

A project this size deserves explicit checkpoints where you decide whether to continue. Suggested criteria:

End of Phase 0: if writing down the typing rules takes more than three months and still feels unsettled, the framework is wrong. Either redesign or stop.

End of Phase 1: if symbolic shape arithmetic doesn't work on real programs (i.e., SMT timeouts on operations smaller than a 100M-parameter transformer), the SMT-based design is wrong. Decide between a less expressive type system or a more powerful (and slower) verifier.

End of Phase 2: if AD-as-effect doesn't produce numerically correct gradients, the framework's central thesis is wrong. The CPS-AD bridge is the load-bearing claim of the whole project; if it doesn't work in practice, the project as designed is dead.

End of Phase 3: if sharding inference doesn't outperform manual annotation on real workloads, the type-inference approach is unproductive. Fall back to mandatory annotation (which is still useful but is a much smaller contribution).

End of Phase 5: if hardware lowering can't get within ~2x of hand-tuned kernels for representative ops, the capability-type approach is too abstract. This is the most likely failure point and the one with the least clear fallback.

The graveyard of failed languages is real. Failure here looks like an interesting research artifact and a few good papers; not a tragedy, but worth being explicit about so the work doesn't drift into unfocused maintenance.

13. The honest one-paragraph recommendation

If you were going to do this seriously: start with Phase 0 in your spare time, write the core calculus over two months, and stop there to decide whether to continue. Phase 0 is the highest-leverage work in the entire program, costs little compared to the others, and tells you almost everything about whether the framework holds up. If at the end of Phase 0 the calculus reads cleanly and the typing rules feel right, Phase 1 is worth the four-to-six-month investment. If it doesn't, you've spent two months on a design exercise that produced a useful written artifact, and you can move on without sunk cost.

The rest of the phases are downstream of that decision. Don't commit to Year 5 from Year 0; commit to Phase 0, then Phase 1, then reassess. Most language projects fail because they overcommit on the strength of the initial design vision; the way to not be one of them is to gate continuation on the actual results, not on the original intent.

You already have all the relevant prerequisites — compiler engineering, formal verification, a habit of writing specs before code, an OCaml-LLVM toolchain pipeline that's structurally what Phase 1 needs. The question is not whether you can do it, but whether it displaces something else that has higher value to you. That's not a question this document can answer.

End of roadmap.