Named dimensions
Tensor axes carry semantic names. A batch by feature matrix and a feature by batch matrix are different types, so a wrong multiply fails before it reaches data.
A functional tensor language for model-written code
A language for programs machines write.
Chelis is a statically typed functional language for numerical code that agents can generate and people can audit. Surf stays readable. Deep gives tools a typed program tree. The compiler checks shapes, precision, effects, ownership, and differentiability before anything runs. The language semantics are mechanized in Lean 4.
hidden = matmul(norm1, ff1) |> relu |> matmul(ff2)
residual = add(norm1, hidden)
out = layer_norm(residual, gamma2, beta2)
outWhy it exists
The author changed.
Python was designed for careful humans writing code directly. Chelis starts from a different workflow: models generate code at high volume, and people supervise the result. That puts the compiler inside the authoring loop.
Every program has a readable surface and a typed machine form. A model can search and rewrite the program as data. A person can review the Surf. The compiler gives structured feedback that both can use.
This is the substrate layer for verification, where guarantees become structural rather than aspirational.
Type system
Checked before runtime.
Precision
Numeric precision is part of the signature. An f32 path cannot quietly absorb an f64 value and keep going.
Effects
Randomness, device resources, and differentiable regions are visible to the compiler instead of buried in library calls.
Linearity
Values that must be used once are checked that way. In-place reuse and resource movement have a type-level contract.
Differentiation
Differentiable regions are visible to the compiler. The supported AD fragment is mechanized against a formal specification.
Surf and Deep
Readable for people. Structured for tools.
Surf is the syntax people read, write, and review. Deep is the canonical typed tree that the compiler and agent tooling manipulate. Surf lowers to Deep and can be decompiled back, so the human view and machine view stay tied to the same program.
This is the practical reason Chelis can serve both adoption paths: humans get a compact functional language, while tools get a program representation they can inspect, mutate, and score.
Ecosystem
The proving ground is real code.
Numerics
nautilus
Scientific methods, statistics, and optimization in pure Chelis, differentiated through the tensor graph.
Dataframes
coral
Typed tables whose numeric columns are tensors, so a dataframe pipeline joins the tensor graph.
Deep learning
school
Typed layers, real grad, optimizers, and training loops on the same checked tensor graph.
Quant finance
shoals
Pricing, risk, curves, and stochastic processes on typed tensors the compiler differentiates.
Requirements
c-earchin
EARS requirements translated into executable Chelis properties with provenance to the source line.
Compiler validation
hull
A reference type checker and evaluator in Chelis, run alongside the compiler to catch drift.
Availability
Prebuilt binaries, three backends.
Chelis ships as prebuilt compiler binaries for Linux x86_64 and macOS arm64, building C, HIP, or Metal output for the environment that runs it.
Available today to early partners of C Proof.
Research
The language has a proof beneath it.
The Lean 4 formalization mechanizes the calculus behind Chelis. The core type-system guarantees rest on machine-checked theorems.
- type soundness well-typed programs do not get stuck
- dimension safety named tensor shapes line up
- effect correctness effects occur only where allowed
- linearity soundness linear values keep their usage discipline
- AD correctness differentiation follows the formal specification