Theory

Copy Markdown

Theory Core IR is an Elixir-oriented meta-compiler for deriving computation code from formal evidence.

The project direction is not to prove the whole Rust language. A complete proof of Rust would require redoing the ownership model, unsafe aliasing/provenance rules, compiler semantics, LLVM memory semantics, trait solving, and large parts of the existing formal Rust ecosystem. That is not the short bridge.

The short bridge is narrower: define a small certified Core IR, prove its local judgments with Theoria, and lower checked programs into Rust, C, or LLVM IR under explicit backend boundaries.

Installation

After publication, add theory to your dependencies:

def deps do
  [
    {:theory, "~> 0.1.0"}
  ]
end

Theoria

Theoria: https://github.com/elixir-vibe/theoria

Theory uses Theoria as the proof kernel for Core IR obligations. Theoria should not be treated as a Lean replacement for large mathematical libraries. Its role here is to check compact certificates generated by Elixir tooling.

A near-term prerequisite is a minimal Prelude for the proof surface:

  • Option
  • Prod
  • Exists

Until those are available, existential statements can be represented as explicit certificate records.

Core Claim

Theoria proves a small and hard Core IR. Elixir generates that IR and the corresponding proof obligations. Backends then lower the certified IR into computation targets.

Elixir DSL / macros
  -> Core IR
  -> Theoria obligations
  -> checked certificates
  -> Rust / C / LLVM IR

This frames Rust, C, and LLVM IR as lowering targets rather than the primary objects of proof.

Certified Core

The Core IR should stay small enough to audit and strong enough to express real systems code. The initial surface should include:

  • typed SSA / ANF
  • total functions
  • algebraic data
  • ownership tokens / affine capabilities
  • region and lifetime judgments
  • effect rows: alloc, read, write, free, call
  • explicit no-UB obligations

Proof Surface

Theoria should check judgments over Core IR programs, including:

  • well_typed
  • borrow_graph_valid
  • initialized_before_read
  • no_use_after_free
  • bounds_safe
  • no_alias_for_mut
  • effect_allowed
  • lowering_preserves_semantics

These judgments are scoped to the Core IR. They do not imply that arbitrary Rust, C, or LLVM IR programs are verified.

Backend Strategy

Stage 1: Safe Rust

Generate safe Rust first. This lets rustc continue to enforce borrow checking, MIR validation, and ordinary code generation. Theoria proves that the Elixir source IR satisfies its own resource, bounds, and protocol obligations before lowering.

This stage is suitable for IDR systems, state machines, protocols, codecs, CRDTs, schedulers, and other bounded systems code.

Stage 2: Unsafe Rust With A Tiny Runtime

Unsafe Rust should be introduced only behind a small trusted runtime surface. Each unsafe primitive must have an explicit contract and a corresponding proof or audit boundary.

Stage 3: C / LLVM IR

C and LLVM IR require stronger backend discipline. LLVM in particular exposes undef, poison, provenance, alignment, lifetime, and UB-sensitive behavior.

The conservative path is translation validation: each generated artifact should produce backend-specific obligations, instead of assuming the lowering pass is correct by construction.

Boundary

Theory should prove its own computation manifold: the Core IR, its certificates, and the preservation properties of selected lowering paths.

It should not claim to prove all of Rust, all of C, or all of LLVM. Those languages remain projection targets. The certified object is the Core IR and the checked path from Elixir into those targets.