daitai-lang
A statically-typed, deterministic language with bra-ket primitives.
What it is
daitai-lang is a general-purpose language with 39+ algebraic keywords, no null, no exceptions, and no implicit coercions. Optional values are Optional<T>. Failable operations return Result<T, E>. Everything else type-checks by structural rewrite, not by hope.
State is immutable by default. Mutation happens through explicit transition functions of the form State × Event → State, which means every change in your program can be replayed, reasoned about, and compared to a specification. The language ships with bra-ket literals —|0⟩, |1⟩, ⟨ψ| — as first-class syntax, because the algebra underneath the language treats quantum and classical state in the same vocabulary.
Why it exists
Mainstream languages took the position that "practical" means accepting runtime errors as part of life. Rust pushed back on memory safety; Haskell pushed back on side effects. daitai-lang pushes back on the next thing: the program as an opaque imperative trace. If a function says it returns a Distribution<Int>, the type system knows this is a sort in the daitai algebra and unlocks the rewrite rules that come with it — including the ones the compiler uses to optimize and the ones the prover uses to verify.
The result is a language where the same source code can be compiled to a binary, exported to a proof obligation, fingerprinted into a CEA vector, and shipped to production — all from one tree, all checked against the same algebra.
A code example
# A two-qubit register, prepared in a Bell state.
type Register = Tensor<Qubit, Qubit>
fn bell() -> Register {
let q0 = |0⟩
let q1 = |0⟩
let h = H(q0) # superposition
let r = CNOT(h ⊗ q1) # entangle
r
}
# Step semantics: classical observation collapses the state.
let step : Register × Measure -> Distribution<Bit × Bit> = observe