CENTL design

Objective

CENTL is an exact-first calculator and numerical language for interactive work, scripts, and machine tools. Its implementation must preserve a sharp boundary between exact results, rigorous enclosures, and indeterminate results.

The implementation is intentionally polyglot. Each language has one bounded role chosen for its strengths.

Architecture

terminal / script / JSON
          |
          v
      OCaml host
 parser, I/O, sessions, limits,
 protocols, rendering, precision
          |
          v
  extracted F* core
 AST, exact semantics and
 transformations, validation,
 proof-backed algorithms
          |
          v
   narrow OCaml/C boundary
          |
          v
 FLINT / Arb / Calcium
 balls, symbolic numbers,
 advanced numerical algorithms

Julia and Nemo form an independent laboratory for exploring algorithms, generating adversarial cases, and checking production results. They are not a runtime dependency of the shipped centl executable.

Responsibilities

F*

The F* core defines what CENTL means. It owns:

• the typed AST and value classifications;
• exact integer, decimal, and rational semantics;
• exact univariate polynomial normalization and bounded expansion;
• exact equation classification and witness-validated real-quadratic completion;
• local mathematical conditions used to justify symbolic simplification;
• validation of values returned across the numerical boundary;
• exact outward conversion of validated dyadic bounds to a decimal scale; and
• stated semantic and representation properties of those definitions.

Proofs are shipped beside the executable definitions and erased during OCaml extraction. The extracted interface must accept and return simple, unrefined boundary types whose invariants are checked at entry.

The current verified boundary begins at the AST. The handwritten OCaml parser converts source literals directly to arbitrary-precision integer pairs without passing through floating point, then F* evaluates and reduces the result. The parser, host result union, renderers, and protocol serializers remain explicit parts of the trusted boundary.

The 0.4.0-dev slice adds a native Arb boundary. The host walks the resolved AST, supplies exact rational inputs and a binary working precision, and receives exact dyadic lower and upper endpoints. The F* core checks endpoint ordering and the exponent budget before the host creates an outward-rounded decimal view.

OCaml

OCaml is the application and extraction host. It owns:

• the executable entry point;
• parsing, statement assembly, and source-location metadata;
• terminal input, history, completion, and cancellation;
• file and script loading;
• resource budgets plus approximation precision requests and retries;
• the host result union, JSON schemas, and request/response transport;
• terminal-aware semantic coloration and plain-text fallback;
• coordination between the extracted core and numerical backend;
• native application packaging.

OCaml must not independently redefine CENTL arithmetic. Human text, color, JSON, and MCP are derived from the same typed host result, while canonical mathematical structures come from the extracted core. For a positive quadratic discriminant, OCaml may compute arbitrary-precision integer floor-square-root candidates after enforcing the exact-bit budget. The extracted core validates the consecutive-square inequalities and derives the solution representation; OCaml only validates and presents the returned boundary value.

FLINT, Arb, and Calcium

The numerical backend owns algorithms that should not be reimplemented without a compelling correctness or performance reason:

• arbitrary-precision real and complex ball arithmetic;
• elementary and special functions;
• algebraic and symbolic exact numbers;
• polynomials, matrices, number fields, and number-theoretic operations.

The binding surface is deliberately small. It exchanges tagged requests and exact representations of results, never host-language floating-point values or preformatted decimal answers.

Julia and Nemo

The laboratory owns no production semantics. It is used to:

• prototype numerical operations;
• generate reference values and difficult inputs;
• compare independent evaluation paths;
• investigate precision growth and performance;
• reproduce suspected backend defects.

Value model

CENTL has no general-purpose semantic float value.

ExactInteger
ExactRational
ExactSymbolic
ExactSequence
ExactSolutionSet
RealEnclosure
ComplexEnclosure
Indeterminate

Every evaluation result carries two independent descriptions. Provenance says how and where CENTL produced the value. Transformation resolution says whether the requested operation was computed, transformed, unchanged_proved, left residual, unsupported, or indeterminate. Exactness is a property of the value and never implies that a requested transformation completed.

An exact solution set contains a typed solution union. Rational solutions keep their normalized numerator and denominator. A nonsquare positive quadratic discriminant produces two equation-local RealQuadratic values with a shared reduced center and positive reduced radicand, distinguished as lower and upper branches. They denote center - sqrt(radicand) and center + sqrt(radicand). This is not yet a general algebraic-number scalar type, so it cannot silently enter ordinary arithmetic or definitions.

An exact sequence is a bounded ordered collection of exact scalar integers, rationals, or symbolic values. It is a result value rather than a scalar expression: arithmetic and approximation do not implicitly map across it, and nested sequences are not part of the current value model.

Conditions attached with assuming remain part of the symbolic result. A simplifier may use a condition only for a rule it establishes directly, and the condition remains visible in both human and machine output.

Approximate real values cross the backend boundary as exact dyadic data: signed integer mantissas, binary exponents, and a nonnegative radius. Decimal strings are created only after the F* core validates this representation.

Evaluation

1. Parse source text into a checked AST.
2. Evaluate with exact values for as long as the operation permits.
3. Preserve a symbolic exact value when the backend can establish one.
4. Request a rigorous enclosure when approximation is explicit or necessary.
5. Increase working precision until the requested output contract is met, a resource limit is reached, or further refinement cannot decide the result.
6. Render only information justified by the exact value or full enclosure.

Symbolic transformation boundaries classify their own outcomes while the operation is still visible. Evaluation propagates the strongest classification to the host result; human, JSON, JSON Lines, and MCP render that same typed metadata. Final-value inspection is not used to guess whether a transformation completed.

Predicates over enclosures are three-valued: certainly true, certainly false, or unknown. Unknown is never silently treated as false.

Human and machine interfaces

The human interface is calculator-first. A script is a saved sequence of the same expressions and immutable definitions accepted by the REPL. Definition state belongs to one calculator, script, stateful JSON Lines process, or MCP process. The one-shot and legacy streaming --json forms remain stateless.

The calculator, piped human input, and files share syntax-aware statement assembly, so an incomplete expression may continue on following lines without a separate continuation grammar. Interactive terminals add completion from the syntax catalog and current session definitions plus private, bounded history that locked updates merge across calculator processes before atomic replacement. Human syntax and runtime mathematical diagnostics retain source name, line, column, and a caret excerpt; machine errors expose the stable zero-based byte position when a source location applies.

The machine interface uses versioned JSON over standard input and output. It returns structured exact values, transformation resolution, enclosure endpoints, precision metadata, stable error codes, and explanatory messages. Pretty terminal output is never parsed by machine clients.

Terminal coloration is derived from typed result fragments: numbers, symbols, functions, operators, and punctuation. ANSI codes are never stored in values or emitted by the JSON interface, and color does not alter evaluation or canonical plain text.

The MCP adapter maps JSON-RPC tool calls onto the same stateful request engine. It does not parse human output or create another evaluation path. A future local service can use the same boundary.

MCP tool discovery publishes closed discriminated output schemas for this same result union, including rational and real-quadratic solution members. Schema trees are built lazily only when tools/list is requested, keeping ordinary human and JSON startup independent of MCP-only metadata allocation.

Persistent stdio uses one FIFO evaluator so definitions and resets remain deterministic. A separate bounded input reader may only mark cancellation tokens for identified active or queued evaluations; it never evaluates expressions or mutates session bindings. The evaluator observes those tokens at cooperative checkpoints and immediately before committing a definition. MCP cancellation responses are suppressed as required by the protocol, while JSON Lines returns a structured cancelled error for the target request. Pending input is bounded by both the 10,000-request process ceiling and a 16 MiB byte ceiling. One valid cancellation may occupy a separately accounted emergency slot when ordinary input has filled either ceiling, so saturation cannot prevent it from marking its target; the per-request byte limit still bounds that slot. Terminal queue overload cancels cancellable work and drains one ordered overload marker instead of retaining an unbounded stream.

Persistent definitions are also bounded in aggregate, not merely by binding count. A commit preflights the session's retained expression nodes, exact-value bits, and symbol/render bytes against the active ceilings, then rechecks cancellation before mutating the session.

Trust boundary

F* can prove properties of CENTL's own executable core, but it cannot prove an external numerical library merely by calling it. The initial trusted base is:

• F*, its extraction process, and its selected Z3 version;
• the OCaml compiler and runtime;
• the narrow C binding;
• FLINT, Arb, Calcium, GMP, and MPFR;
• the platform compiler and linker.

CENTL reduces this risk with narrow interfaces, range and representation checks, property testing, fuzzing, differential evaluation, and precision-independent identities. Basic verified interval operations may later move into F* to shrink the numerical trust boundary.

Planned source layout

src/fstar/       verified language core
src/ocaml/       executable host
src/native/      numerical binding shim
lab/julia/       independent Nemo experiments
tests/           golden, property, differential, and adversarial tests
docs/            design and user documentation

Non-negotiable rules

• Decimal source literals never pass through binary machine floats.
• Approximation is visible in both source intent and result representation.
• Precision is a request and a verified outcome, not an unsupported promise.
• No layer may convert an enclosure to a point value silently.
• Resource exhaustion produces a structured indeterminate result.
• The human renderer and machine protocol are views of the same result object.