Specification
What the language is committed to
Phase 0 is the formal core calculus. Phase 1 is the implementation contract for the OCaml compiler, Rust runtime, and Lean 4 track. Design memos come first if you want the thesis before the rules.
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: 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: 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