disp is under heavy development and much of the codebase is AI-written — explore this website at your peril :)

disp

abbr.

disp is an aspiring general-purpose programming language with and , and a based on that models hardware as imperfect interaction-net reduction. Based on Barry Jay's tree calculus.

Read the Docs
$ git clone github.com/libdither/disp && npm i && npm test
starting engine… Playground

Why disp?

The goal of disp is a language where you write only the specification and the implementation is derived from it. A specification is a type, and in disp a type is a predicate you can run, so the type checker is an ordinary function from programs to a yes or a no. Multiply that verdict by a cost score from a model of the hardware, and "find the best program" becomes a search with a fitness function. Because the checker, the cost model, and the search are all disp programs, the search can be aimed at itself: an optimizer that improves its own optimizer, and stays readable while it does.

Everything else about disp exists to make that loop close: the tree calculus underneath (programs are data, with no quote/eval border), types as predicates, a trusted kernel small enough to audit, and the plan for user-definable syntax. A survey of the neighbouring languages reduces the goal to five requirements and scores each of them on the same scale, disp included.

  1. G1

    Substrate

    Programs can take other programs apart and run them directly — no encoding step, no separate quote/eval layer — so the type checker is just an ordinary program in the language

    program inspection — metone representation — metchecker as a function — met 100% native
  2. G2

    Specification

    A spec can say everything that matters: types that mention values (dependent types or stronger), proofs you can run, resource and cost budgets, and a workable answer to when two different programs count as the same — with the whole type system built as library code, not baked into the core

    dependent types — metfirst-class proofs — halfway (small library)cost in types — not metequality theory — halfway (witness slices) 55% dependent, library
  3. G3

    Trust

    A verdict is only as believable as the code you must audit to accept it, so that code is kept tiny: every clever layer — elaborator, solver, search — is untrusted and must hand a small core replayable evidence for its claims, and only what the core re-checks counts (the tradition LCF started); a fast path installed in place of a slow definition carries evidence of the same kind

    auditable core — metevidence objects — metindependent re-checking — halfway (one core)evidence-carrying fast paths — halfway (one slice) 80% two-op core
  4. G4

    Execution

    Runs at C/Rust speed, with a model of the target the checker can reason about and a cost account that is exact and replayable rather than a benchmark

    native speed — not metmodel of the target — not metdeterministic cost — met 30% interpreted
  5. G5

    Search

    From spec to implementation automatically: a search over candidate programs scored by the checker (pass/fail) times measured cost — and eventually that optimizer aimed at its own code

    spec → implementation — not metchecker × cost — not metself-application — not met 0% designed

The figure on each row is where disp stands today, one dot per clause of the requirement: filled = met, half-filled = halfway, empty = not met, dashed = still open. The percent is their weighted mean, the word is how it's reached, and hovering a dot names its clause. Text and scores come from _AXES.md.

31 neighbouring projects are scored on the same five axes. None of them combines native reflection with search, the pair disp is built around, and disp is last on equality, where several small projects already have answers. Per axis, these score higher than disp:

See the full comparison