Documentation
Guides

Guides

Clef is being built in the open, on published research. The toolchain is still being assembled, so this section is where to follow the project: where the compiler and language stand today, and the research underneath the design.

For the current state and the ways to engage now, see Getting Started. The language specification and design rationale are the site’s most developed material.

A Deeper Dive - arXiv Pre-Prints

Separate from the entries on this site are a foundational sequence of preprints, formal treatments of key ideas and concepts this site carries through the design, compiler internals and reference materials.

  1. Dimensional Type System and Deterministic Memory Management. (DTS+DMM) The foundation, and the reason Clef has no unsafe escape hatch: memory safety is established at design time, before a single instruction runs. Kennedy-style dimensional types make the code self-describing, so the code performs double duty: it reads to a developer or a domain expert as what a value means, and to the compiler as how to lay it out. That structure then rides multi-stage MLIR lowering all the way down, resolving numeric representation and memory lifetime together as coeffects of our Program Semantic Graph.
  2. The Program Hypergraph. (PHG) Our semantic graph extends beyond detailing compute to include correctness proofs for free, making the structure inherently a hypergraph. Clifford algebra is the sharpest example: a value can carry grade and the compiler transforms the geometric product to limit the substrate to non-zero nodes, an 85-95% reduction in computational burden. The same structure can carry unitarity to a quantum gate, so one verified representation spans a physics kernel, an NPU tile, a quantum-classical workload, as well as ordinary code on standard hardware. Mathematical theory creates computational reality.
  3. Adaptive Domain Models. (ADM) This is our furthest reach, a non-trivial departure from machine learning norms: a training method with no backpropagation. It runs forward only, with gradients on the stack and exact posit accumulation, so the backward pass’s memory blowup never happens and a model’s geometry survives training intact. On that footing it uses dimensional types to build physics-aware models on an established Bayesian framing. We see this as a contribution that provides truly unique value in making “AI” more efficient and sustainable, and brings the prospect of self-improving models with structural integrity along with it.
  4. Decidable By Construction. (DBC) The keystone. It draws the three papers before it into one claim: everything that makes a model numerically stable and physically consistent can be decided in polynomial time, as a design-time advantage. Then it goes further, into territory that surprised us: the ordinary type inference doing that checking turns out to be a form of universal induction, computing the most probable explanation of your program under a computable slice of Solomonoff’s prior. Formalism this deep is what makes the implementation it provides rock-solid.
  5. Fixed-Point Scaffolding. (FPS) Y-Combinator is more than a catchy name for a tech financier. It is the fixed point of the lambda calculus, the algebra at the heart of the ML family, and the small irony of this paper is that we run it straight through MLIR’s C++ undercarriage. The formal structure of Huet’s zipper and Petricek’s codata/coeffect formalism sequences our compiler’s lowering passes, carrying grade, escape, and representation annotations through MLIR. The best part: the whole construction stays an internal scaffold, so at design time the developer gets the guarantees while the category theory remains within compiler internals.
  6. Negative and Fractional Types. (NFT) Another extension our system makes available is the concept of negative and fractional type: one for information that flows backward, one for a resource split into pieces, both first-class citizens of the type system. They come from the James-Sabry dualities in compact closed categories, and the same Kennedy-style abelian-group structure keeps them decidable, principal types and all. Other languages take unprincipled approaches to reversible computation with library machinery that adds bloat and surface area for errors. Our full expression of dimensional types keeps the structure intact while admitting support for Bayesian inference, quantum computation, and even adiabatic computing.

Read together, (and we confess, it’s quite a bit of reading) the six are one program. Our Native Type Universe (NTU) carries dimension, grade, memory, proof obligations and other factors from source through MLIR to whatever processor runs the code. While the Fidelity Framework has always been grounded in utility (garden-variety tasks and systems use cases), the language targets CPU, GPU, NPU, FPGA and microcontrollers today, and shows its reach to support novel AI hardware, quantum processors and other emerging substrates that are on the horizon.