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 Program Semantic Graph retains joint constraints as hyperedges, together with their participants and supporting evidence. Geometric algebra illustrates the benefit: checked blade-support rules can identify structurally zero products before code generation. The same representation is intended to carry domain-specific obligations across ordinary systems code, physics kernels, and accelerator workloads. Quantum unitarity is a possible extension through checked domain laws; a hyperedge alone does not establish it.
  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 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 connects principal dimensional inference to a four-tier verification model: types and admitted structural rules at Tier 1; graph coeffects and local arithmetic obligations at Tier 2; reusable domain and system laws over PSG relationships at Tier 3; and compiler or probabilistic relational reasoning at Tier 4. The compiler generates and dispatches supported obligations from typed code and library use. Application authors need not annotate each operation with a proof. The principal-inference result applies to the dimensional fragment; stronger claims retain their own premises and checking requirements. The paper also distinguishes exact admissibility from Bayesian ranking under a separately declared probability model. The Tier 3/4 library integrations and semantic adapters remain development work.
  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) This research explores value-indexed resource operations and categorical duality for reversible computation and recovery-aware model updates. These extensions need their own laws and semantic interpretations; they do not inherit principal dimensional inference simply by sharing a graph. Bayesian inference, quantum unitarity, and adiabatic approximation are possible application domains, each with additional proof obligations.

Read together, the six describe one program: retain types, resource requirements, and proof evidence through native compilation. Clef and the Fidelity Framework serve general-purpose programming and systems work, with a verification foundation designed to provide automatic coverage through ordinary typed code. Heterogeneous and quantum targets extend that foundation where the required semantics, libraries, and backend implementations are available. Getting Started records the current implementation scope.