Progress & Comparisons
Every language and system that aims near disp's goal, scored on the same five axes (as of August 2026) as a percentage of what disp's final goal state is. Compare against current state of disp and sort by an axis to see who is ahead. The full write-ups are at research/awesome-langs.
| disp self-assessed 53% | 100% native | 55% dependent, library | 80% two-op core | 30% interpreted | 0% designed |
|---|---|---|---|---|---|
| 29% | 33% graph nodes | 0% untyped | 0% trust hvm.c | 70% native, GPU | 40% value enumeration |
| 35% | 0% none | 65% affine dependent | 30% one-file kernel | 40% native, GPU | 40% LLM loop |
| 38% frontier | 33%? deep embedding | 20% HOL subset | 88% tiny C verifier | 50% verified x86 | 0% none |
| 32% | 0% erased | 40% SMT | 0% SMT TCB | 40% Rust | 80% LLM, cost loop |
| 34% | 50% Meta-F* | 65% dependent+SMT | 15% big TCB | 40% via C | 0% human-written |
| 47% | 50% quotation | 65% dependent | 60% small kernel | 20% via C | 40% external agents |
| 30% | 0% none | 70% extensional MLTT | 80%? certificates | 0% none | 0% none |
| 36% frontier | 0%? s-expressions | 80% cubical+QTT | 100% LCF, two checkers | 0% none | 0% tactics |
| 16% | 0% none | 40% dependent+QTT | 0% trusted compiler | 40% LLVM native | 0% none |
| 70% frontier | 50% Gallina meta | 65% CIC | 85% Rocq kernel | 70% beats GCC | 80% randomized |
| 51% | 50% Lean meta | 65% Lean+mathlib | 80% Lean kernel | 0% none | 60% agentic loop |
| 30% frontier | 50% quotation | 80% HoTT | 20% big checker | 0% GHC/JS | 0% none |
| 15% | 0% none | 55% HoTT | 20% big checker | 0% none | 0% none |
| 42% | 33% rewrite patterns | 65% rewriting, library | 72% re-checker | 0% none | 40% ATP export |
| 35% frontier | 33% meta-language | 70% user theories | 70% LCF nucleus | 0% none | 0% none |
| 32% frontier | 50% quotation | 75% dependent+QTT | 15% trusted checker | 20% Chez + erasure | 0% basic auto |
| 40% frontier | 0% none | 40% HOL4+sep logic | 88% HOL4 LCF | 70% verified native | 0% none |
| 21% | 0% none | 50% dependent+linear | 15% trusted checker | 40% to C | 0% none |
| 21% | 0% excluded | 25% contracts, BMC | 0% BMC TCB | 40% Cranelift | 40% CEGIS+LLM |
| 16% | 0% none | 40% SMT | 0% SMT TCB | 0% managed | 40% LLM-written |
| 18% | 0% none | 0% none | 15% metatheory | 55% to C | 20% LLM target |
| 37% | 0% two-layer | 65% refinement–Iris | 38% per tool | 40% Rust | 40% harness gen |
| 28% | 33% staging | 15% comptime values | 12% MLIR stack | 40% MLIR codegen | 40% param sweeps |
| 18% | 50% logic graph | 0% designed | 0% none | 40% Cranelift JIT | 0% none |
| 14% | 0% none | 20% math prover | 0%? own checker | 0% none | 50% local neural |
| 9% | 0% none | 25% SMT contracts | 0% SMT TCB | 20% claimed | 0% none |
| 14% | 17% env only | 25% STLC+refinements | 0% report only | 30% static bounds | 0% none |
| 30% frontier | 83% inert terms | 15% library types | 50% paper theorems | 0% none | 0% none |
| 37% frontier | 83% native eval | 0% structural | 50% spec + jets | 50% native runtimes | 0% none |
| 35% | 0% none | 40% contracts, ladder | 38% trust ledger | 55% via rustc | 40% agent loop |
| 20% | 0% none | 25% Z3 contracts | 0% SMT TCB | 35% host legs | 40% agent loops |
percent of what disp needs on the axis; one dot per clause (hover an axis for them) met halfway not met open ahead of disp small text: how ? a clause the write-up leaves open does not apply (left out of the mean) ᵈ designed, not builtᶜ claimed, unverified provenanceᶠ cost-only parameter sweeps, not program searchᵗ static iteration bounds, no native speed
Also surveyed, unscored: Graveyard.
Pick a language in the table to see its scorecard notes, where disp differs, and the survey's verdict.