Skip to content
Chelis docs

Introduction

Octant is a bridge from mathematical LaTeX to Chelis Deep. It takes a formula written in LaTeX, the form a quantitative analyst already has in a research note, a textbook, or internal documentation, and produces a Chelis Deep s-expression that the Chelis compiler accepts.

The name comes from navigation. An octant reads angular positions from celestial reference points. Octant reads computational meaning from mathematical notation.

LaTeX to Chelis Deep, with provenance

Section titled “LaTeX to Chelis Deep, with provenance”

Octant does two things at once.

First, it translates. A useful subset of mathematical LaTeX, the notation that appears in finance and scientific computing textbooks, becomes a Chelis Deep program with types inferred where the source makes them derivable.

Second, it records where every piece of the output came from. Each emitted Deep node carries a span identifier in its metadata map. A sidecar provenance manifest, written as <input>.spans.json, maps each identifier back to a byte range, a line and column, and an equation label in the original LaTeX. The identifiers are stable. The Chelis compiler preserves them through parsing, type checking, lowering, and code generation, so a node in the generated host source can be traced back to the formula it came from.

That is the point of Octant. "Show me where this number comes from" has a mechanical answer that runs from the LaTeX source through to the generated code.

Where Octant sits

Section titled “Where Octant sits”

A quantitative analyst has a pricing model expressed as LaTeX. They want a verified implementation. Octant takes the LaTeX and produces Deep. The Chelis compiler produces a binary. The analyst reviews the LaTeX, which they wrote or can verify by inspection, alongside a property file that is short and declarative. They never need to read the compiled Chelis.

Octant produces Deep that goes through the same verification chain as hand-written Chelis: type checking, effect and linearity validation, lowering to RISC IR, and code generation. Octant contributes the upstream half of the audit chain, the span-attributed Deep plus the sidecar manifest. The Chelis compiler preserves the spans through its own passes.

Octant ships with a library of canonical reference pairs. Each pair is a LaTeX file alongside a hand-written Chelis implementation that the translation of that LaTeX is expected to match. The reference pairs are both the onboarding material and the correctness oracle for the translator. Several appear as the worked examples in this book.

What this book covers

Section titled “What this book covers”