Specification
What the language is committed to
These documents are contracts for intended semantics. A completed spec is not a completed implementation. For what the tree actually does, start at the current status. Phase 0 is the formal core calculus. Phase 1 is the implementation contract for the OCaml compiler, Rust runtime, and Lean 4 track. Later-phase docs are design, not shipping claims.
Foundation
Phase 0 — core calculus
- Phase 0, Section 1: Type System Foundation
- Phase 0, Section 2: Core Operation Set & Typing Rules
- Phase 0, Section 3: Subtyping and Coercion
- Phase 0, Section 4: Operational Semantics
- Phase 0, Section 5: Implementation Infrastructure
- Phase 0: Foundation — Index
- Phase 0 review checklist — coverage before freeze
- Phase 0 second-reader pass — 2026-05-09
Phase 1 — implementation
- Phase 1, Section 1: Scope, Milestones, and Exit Criteria
- Phase 1, Section 2: Compiler Implementation
- Kina Application Binary Interface (ABI) Stability Policy
- Phase 1, Section 3: Runtime Implementation
- Phase 1, Section 4: Observability — Tracing, Logging, Diagnostics
- Phase 1, Section 5: Operation Set Extensions
- Phase 1, Section 6: Verification Track
- Phase 1, Section 7: Testing, Quality, and Public ABI
- Phase 1, Section 8: Exit Criteria and Phase 2 Entry
- Phase 1, Section 9: `log_softmax` and `take_along_axis`
- Phase 1, Section 10: Restricted reverse-mode VJPs for StoryLM-0 loss
- Phase 1, Section 11: Functional SGD
- Phase 1, Section 12: `reverseMode` result ABI
- Phase 1, Section 13: Tuple projection
- Phase 1, Section 14: Restricted reverse-mode VJPs for the StoryLM-0 decoder graph
- Phase 1, Section 15: NLL ∘ decoder and multi-weight SGD
- Phase 1, Section 16: Functional AdamW
- Phase 1, Section 17: Deterministic `argmax`
- Phase 1, Section 18: Seeded categorical sampling
- Phase 1, Section 19: Functional KV-cache append
- Phase 1, Section 20: Host generation loop
- Phase 1, Section 21: Prefill → decode handoff
- Phase 1, Section 22: `T_max` padded scratch
- Phase 1, Section 23: StoryLM-0 32-token checkpoint rollout
- Phase 1, Section 24: StoryLM-0 host train loop
- Phase 1, Section 25: StoryLM-0 decoder-wide AdamW
- Phase 1, Section 26: StoryLM-0 mean NLL
- Phase 1, Section 27: StoryLM-0 trained 32-token fixture
- Phase 1: Implementation — Index
Later phases
- Implementation Roadmap: From Design Memos to Working Language
- ABI Specification
- Phase 2: Reverse-Mode Automatic Differentiation (AD) as an Algebraic Effect
- Phase 2, Section 1: Scope, Milestones, and Exit Criteria
- Phase 2, Section 2: Effect Handler Infrastructure
- Phase 2, Section 3: Automatic Differentiation
- Phase 2, Section 4: Control Flow and Iteration
- Phase 2: AD as an Effect — Index
- Phase 3, Section 1: Scope, Milestones, and Exit Criteria
- Phase 3, Section 2: Mesh and Sharding Types
- Phase 3, Section 3: GSPMD Propagation
- Phase 3, Section 4: Collective Coercions
- Phase 3, Section 5: StoryLM-0 as the first sharding workload
- Phase 3, Section 6: StoryLM-0 head-parallel attention
- Phase 3, Section 7: StoryLM-0 QKV projection shards
- Phase 3: Sharding (The Distribution Axis)
Design memos
- AI-Native Programming Language: Design Space Series
- Design Space 01: Static vs Dynamic Shapes
- Design Space 02: Differentiation Through Effects
- Design Space 03: Compositional Sparsity and Structured Tensors
- Design Space 04: Distributed Programming Model
- Design Space 05: Verification
- Design Space 06: Hardware Abstraction
- Language Inspirations and Target Matrix
Forward tracks
Decisions
- Architecture decision records (ADRs)
- Implementation / code snapshot change log
- Phase 0 reference implementation status (OCaml compiler)
- Specification Change Log
- ADR: Toolchain pins (LLVM, Z3, Lean)
- ADR: StoryLM-0 loss operations
- ADR: StoryLM-0 loss-op VJPs
- ADR: StoryLM-0 functional SGD
- ADR: reverseMode result ABI
- ADR: Tuple projection for reverseMode results
- ADR: StoryLM-0 decoder-graph VJPs
- ADR: StoryLM-0 NLL ∘ decoder train step
- ADR: StoryLM-0 functional AdamW
- ADR: StoryLM-0 deterministic `argmax`
- ADR: StoryLM-0 seeded categorical sampling
- ADR: StoryLM-0 functional KV-cache append
- ADR: StoryLM-0 host generation loop
- ADR: StoryLM-0 prefill → decode handoff
- ADR: StoryLM-0 `T_max` padded scratch
- ADR: StoryLM-0 as the first Phase 3 sharding workload
- ADR: StoryLM-0 head-parallel attention
- ADR: StoryLM-0 QKV projection shards
- ADR: StoryLM-0 32-token checkpoint rollout
- ADR: StoryLM-0 host train loop
- ADR: StoryLM-0 decoder-wide AdamW
- ADR: StoryLM-0 mean NLL
- ADR: StoryLM-0 trained 32-token fixture