Theoria

Copy Markdown View Source

Theoria is an Elixir-native proof/spec kernel inspired by Lean's trusted-kernel architecture.

The goal is not Lean compatibility. Theoria starts as a small, reliable core for checking proof terms generated by Elixir DSLs, tactics, and domain-specific specification tools. The first target domains are finite data structures, graph algorithms, compiler passes, and static-analysis invariants.

Theoria is intentionally split into a small trusted kernel and future untrusted convenience layers. DSLs and tactics may generate proof terms, but only the kernel can admit checked declarations.

Installation

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

Design principles

  • Keep the trusted kernel small.
  • Treat DSLs, macros, tactics, and automation as untrusted proof generators.
  • Admit a theorem only after the kernel checks its proof term.
  • Use precise Elixir structs and result tuples so the codebase is friendly to Elixir's gradual set-theoretic type direction.
  • Grow through tests and proof corpora before adding convenience layers.

See docs/design.md for the current design notes.

Current status

The initial kernel supports:

  • universe terms (Type n as Sort n)
  • de Bruijn bound variables
  • constants
  • lambda abstraction
  • dependent function types (forall)
  • application
  • beta reduction
  • definitional equality by normalization
  • checked constants and definitions in an environment

Example core term

import Theoria.Term

identity_type =
  forall(:a, sort(0),
    forall(:x, bvar(0),
      bvar(1)
    )
  )

identity_proof =
  lam(:a, sort(0),
    lam(:x, bvar(0),
      bvar(0)
    )
  )

:ok = Theoria.Kernel.check(Theoria.new_env(), identity_proof, identity_type)

Quality checks

The repository includes a Reach-style CI alias:

mix ci

It runs compilation with warnings as errors, formatting, Credo, ExDNA, Reach architecture/smell checks, Dialyzer, and tests.

Roadmap

  1. Harden the kernel with more normalization, substitution, and negative tests.
  2. Add equality and basic logical connectives.
  3. Add primitive Bool/Nat/List theories.
  4. Add a small Elixir DSL that elaborates to checked core terms.
  5. Add finite graph/spec libraries for tools such as Reach.