Research language · incomplete

Tensors that already know their shape.

Kina is a research language for typed tensor programs. The bootstrap compiler is OCaml; it checks dtype, shape, and placement with Z3 and emits textual MLIR. A Rust runtime and a Lean 4 track sit beside it. The language is not finished: you can compile tensor graphs, including a tiny causal-attention forward pass, but you cannot yet train or serve a language model in Kina.

Current status Browse examples Surface syntax

Phase 0 spec completePhase 1 compiler emits MLIRStoryLM-0 is a forward graph

From the StoryLM-0 forward graph — compile and numerical check, not a trained model

let logits = fn(
  token_ids: tensor<I64, [1, 4], @host>,
  token_embedding: tensor<F32, [8, 4], @host>,
  wq: tensor<F32, [4, 4], @host>
) -> tensor<F32, [1, 4, 4], @host> {
  let x = token_embedding.gather(token_ids) in
  let q = x @ wq.broadcast([1, 4, 4]) in
  q
}