Non-normative. Assessed 2026-08-23 against the in-tree compiler, runtime, verification track, and public site. If this page and a numbered specification disagree, the specification still wins for intended semantics. This page wins for “what is actually wired.”
Kina is a research compiler with a public documentation site, not a finished programming language. You can compile typed tensor graphs to textual MLIR, run a 32-token host rollout from a patterned fixture, and fit a toy eight-class corpus with host SGD or AdamW. You cannot yet serve a useful language model in Kina.
One-line status
Phase 0’s formal spec is written. Phase 1 has a real OCaml compiler that emits MLIR, but Phase 1 exit criteria are not met. A bootstrap .kina surface is implemented ahead of the Phase 7 surface-language phase. Early Phase 2 control flow and a restricted reverse-mode AD pass exist in the compiler.
What a visitor can do
| You can | You cannot |
|---|---|
| Read the Phase 0 calculus and Phase 1 implementation contract | Treat those specs as a completion claim |
Write .kina tensor programs the compiler already accepts |
Assume modules, packages, a real stdlib, LSP, or a REPL exist |
| Type-check shapes and dtypes, including some symbolic dims via Z3 | Rely on full refinement predicates in the typed IR |
Emit textual MLIR and, when the LLVM/MLIR tools are present, a .so |
Assume a complete GPU runtime or PyTorch-parity transformer demo |
Compile storylm0_forward.kina and numerically check logits |
Tokenize real text |
Compile host log_softmax / take_along_axis and restricted VJPs for NLL |
Device take_along_axis, or train |
| Compile functional SGD and functional AdamW and check the update numerically | Run AdamW through reverseMode |
Run a restricted handle … with reverseMode transform, name (y, g), and apply SGD in one wrapper fn |
Differentiate an arbitrary program |
| Compile decoder-graph VJPs and a host NLL∘decoder step that SGDs or AdamWs every trainable weight | Device ScatterAdd |
Compile host argmax and check greedy token ids numerically |
Draw uniforms inside Kina, or emit prose |
| Compile host Gumbel-max sampling and check seeded token ids | Top-k / top-p, or an in-graph PRNG |
| Compile a one-step KV-cache append and check attention numerically | Grow the cache inside while |
Compile prefill handoff and a T_max pad / unpad |
Write in-place, or grow S inside while |
| Load the StoryLM-0 fixture and greedy-roll 32 tokens | Serve a model, or tokenize real text |
Compile mean NLL as keepdims reduce_sum times host 1/(B·T) |
A reduce_mean VJP, or treat Sections 24 / 25 as mean training |
| Fit the toy corpus with host NLL∘SGD or NLL∘AdamW and greedy-roll the taught cycle | A useful LM |
Compile 2-way column-parallel lm_head and match unsharded logits |
Parse @mesh / @sharded, or run the 4-device simulator |
| Compile 2-way head-parallel attention and match unsharded logits | Combine vocab + heads, or parse @mesh |
| Compile 2-way column-parallel QKV and match unsharded logits | Shard Wo (needs all-reduce), or run the 4-device simulator |
The public site at kina.acaldwell.dev is a reading surface for docs, examples, and goldens. It does not compile or execute programs in the browser.
Types that exist today
Implemented tensor types carry dtype, shape (static or symbolic), and host / device placement.
Specified or sketched, but not finished in the typed IR:
- Refinement predicates
R(Phase 0) - Effect rows as a complete algebraic-effect system (Phase 2)
- Sharding (Phase 3)
- Sparsity (Phase 4)
- Hardware capability (Phase 5)
Effect-row syntax (!{…}), perform, and handle parse and have early lowering. That is not the Phase 2 AD-as-handler design.
Surfaces
Two concrete syntaxes reach the same Ast_surface AST:
.kinatext — the user-facing bootstrap surface. Grammar:01-surface-kina.md. Selected when the input file extension is.kina.- S-expression core — the older Phase 0 IR. Grammar:
02-surface-kina.md. Still accepted bySexpr_parser.
The roadmap still lists a Phase 7 surface language (inference, error quality, LSP, a frozen grammar). The current .kina syntax is a bootstrap pulled forward so examples and the site have a readable language. It is not that Phase 7 freeze.
Known bootstrap limits that visitors hit:
{ 1.0 }payload syntax on tensor literals is parsed and discarded. Literals are typed placeholders unless a later host injects values.src/compiler/lib/stdlib/stdlib.kinais a sketch inlined by the CLI, not a packaged standard library.
Compiler, runtime, verification
Compiler (src/compiler/)
- Pipeline: parse →
Type_formation.check_program→ optionalAd_pass.transform_ad→Emitter.emit_tensor_program→ optional.soviaPipeline.compile_mlir_to_so. - Ops that compile today include elementwise arithmetic, rank-2 and batched rank-3 matmul, reductions (including host
argmax→I64), transpose, reshape, broadcast, slice, concat, 2Dgather,softmax, hostlog_softmax, hosttake_along_axis,repeat_interleave, casts, and the usual transformer unaries (relu,sigmoid,silu,gelu,rsqrt, …). - Control forms:
fn,let,if,while, tuples,handle/perform. - Reverse-mode AD is a static compiler pass over a restricted let-bound graph (add, mul, variadic-batch matmul including rank 4, transpose, broadcast, sum, softmax,
log_softmax,take_along_axis, reshape, 2Dgather, relu, sigmoid, rsqrt,neg). Other ops fail the pass.reverseModereturns the flat tuple(primal, g…)for floating parameters; discreteI64parameters are omitted. MLIR multi-resultfunc.func. A destructuringlet (y, g) = …can name those results outside the differentiated function. Gather’s cotangent is IR-internalScatterAdd.
Runtime (src/runtime/)
- More than a Phase 0 heap stub: tensor/DLPack types, FFI dispatch, optional CUDA paths, and an experimental fiber module.
- Not the completed Phase 1 runtime contract (stress tests, pool-allocator gate, Miri/
Send+Syncstory, library-author guide).
Verification (src/verification/)
- Lean 4 project builds theorem statements. Subject reduction is still
sorry. This is not the Phase 1 non-trivial proof gate.
StoryLM-0 versus StoryLM Lab
Two different things share a name:
tests/compiler/examples/storylm0_forward.kina— a tiny causal multi-head attention forward graph (token gather, host-provided causal mask, vocab logits). Compile-only in the language;scripts/validate_storylm0_forward.pychecks numeric logits against a reference.experiments/storylm/— a Python / Hugging Face evaluation harness for creative-writing prompts. It does not train or run a Kina model.
log_softmax and take_along_axis are specified in
09-log-softmax-and-take-along-axis.md
and compiled on the host. NLL is -log_softmax.take_along_axis. Restricted
VJPs for neg, log_softmax, and take_along_axis are specified in
10-log-softmax-and-take-along-axis-ad.md.
Functional SGD is specified in
11-functional-sgd.md
as w - lr.broadcast(σ) * g. The reverseMode result ABI is specified in
12-reversemode-result-abi.md:
a wrapper fn can return primal plus parameter gradients from a .so.
Destructuring let (y, g) = … is specified in
13-tuple-projection.md
and can feed g into functional SGD. Restricted VJPs for reshape,
variadic-batch matmul (including rank 4), and 2D gather are specified in
14-decoder-ad.md.
storylm0_ad_step.kina runs the decoder graph and SGDs the embedding
table. storylm0_nll_step.kina composes Section 9 NLL with that
graph and SGDs every trainable weight (sum of per-token NLL; seed
ones). Functional AdamW is specified in
16-functional-adamw.md
as existing arithmetic; adamw_step.kina updates one [4, 8]
parameter and its moments. Decoder-wide AdamW is specified in
25-storylm0-decoder-adamw.md;
storylm0_adamw_step.kina applies that update to every
trainable weight. Host argmax is specified in
17-argmax.md;
storylm0_greedy.kina selects class ids from [1, 4, 8] logits
(lowest index on ties). Seeded categorical sampling is specified in
18-seeded-sampling.md
as host Uniform + Gumbel-max + argmax; storylm0_sample.kina
draws [1, 4] ids from host noise and temperature. Functional
KV-cache append is specified in
19-kv-cache.md
as concat plus one new-token attention; storylm0_kv_step.kina
appends S=1 onto a static past cache. The host generation loop
is specified in
20-host-generation-loop.md;
storylm0_generate.kina greedy-rolls three tokens from one seed
via static-S decode plus argmax. Prefill → decode handoff is
specified in
21-prefill-handoff.md;
storylm0_prefill.kina returns the T=3 cache and one decode
step. T_max scratch is specified in
22-tmax-scratch.md
as pad-with-zeros + slice-prefix; storylm0_tmax.kina keeps a
[…, 5] cache next to the live prefix. The companion
32-token test is specified in
23-storylm0-rollout.md;
storylm0_rollout.kina re-forwards a static T=36 graph
from a patterned NPZ fixture. The host train loop is
specified in
24-storylm0-host-train.md;
just validate-train fits three sliding windows and greedy
continues once upon a time the end. just validate-decoder-adamw
does the same loop with Section 16 AdamW. Mean NLL is specified
in
26-storylm0-mean-nll.md;
storylm0_mean_nll_step.kina keepdims-sums per-token NLL and
scales by host 1/(B·T). The trained 32-token fixture is
specified in
27-storylm0-trained-fixture.md;
just validate-trained-rollout loads storylm0-checkpoint-v1
and locks the taught cycle over 32 generated tokens. The first Phase 3
workload is specified in
05-storylm0-workload.md
as 2-way column-parallel lm_head; storylm0_tp_vocab.kina
matches the unsharded forward. Head-parallel attention is
specified in
06-storylm0-head-parallel.md;
storylm0_tp_heads.kina slices Q/Kᵀ/V on the head
axis. Projection shards are specified in
07-storylm0-proj-shards.md;
storylm0_tp_proj.kina slices Wq/Wk/Wv on the
H·Dh axis. @mesh / @sharded are not in the compiler.
Still missing: reduce_mean VJP, top-k / top-p,
in-place write, a real corpus, mesh types.
llm_generate.kina is a loop-carried matrix sketch, not token-level generation.
Phase checklist (honest)
| Phase | Spec | Implementation |
|---|---|---|
| 0 Foundation | Complete | Core ops and shape checking exist; refinements R are not in the emitting IR |
| 1 Shape-typed compiler | Complete as a contract | Compiler → MLIR is real; GPU transformer vs PyTorch, performance band, ABI/docs gates are open |
| 2 AD as an effect | Drafted | Early AST + restricted compiler AD; not handler-based AD |
| 3 Sharding | Design docs + StoryLM-0 vocab / head / proj-shard algebra | Mesh types not built |
| 4–6 Sparsity, hardware, proofs | Roadmap / partial Lean | Not built (Lean is statements) |
| 7 Surface language | Deferred in the roadmap | Bootstrap .kina exists; freeze, inference, and tooling do not |
Where to read next
- Syntax:
01-surface-kina.md, then the S-expression core02-surface-kina.md - Code map:
00-CODEBASE.md - Implementation gap ADR:
32-phase-0-reference-implementation-status.md - LLM readiness (dated 2026-07-15):
47-creative-writing-llm-assessment.md - Examples:
tests/compiler/examples/