AI-native language

Tensors that already know their shape.

Kina is a programming language for machine-learning programs whose types carry shape, refinements, effects, and hardware. The bootstrap compiler is OCaml; it type-checks with Z3 and emits textual MLIR. A Rust runtime and a Lean 4 track sit beside it. This site is the public face of that work — not just the odoc pages for the compiler library.

Start learning Browse examples Surface syntax

Phase 0 spec completePhase 1 compiler → MLIRStoryLM-0 vertical slice

From the StoryLM-0 forward graph

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
}