A research language for knots and their mathematics — topological, algebraic, geometric and logical — in which programs are structured objects and equivalence is defined by transformation.
Tangle is an experimental, Turing-complete programming language in which:
programs are structured as tangles (braids), and program equivalence is defined by isotopy.
Rather than treating programs as sequences of instructions, Tangle treats them as composable topological objects. This allows reasoning about programs in terms of structure, equivalence under transformation, and invariants of representation.
Its remit is deliberately broad: Tangle aims to be a general language for doing mathematics about knots — not a front end to any particular knot database.
computation is construction of structured objects, and meaning is preserved under valid transformations.
In this setting:
-
programs are graphs/braids
-
execution corresponds to transformation
-
equivalence is not syntactic equality, but structural equivalence
This aligns with concepts from knot theory (Reidemeister moves), category theory (morphisms and composition), and algebraic invariants (classification via structure).
Tangle is a separate project from KRL and QuandleDB. The three share a subject matter, not an architecture.
| Project | What it is |
|---|---|
Tangle (this repository) |
A general language for knot mathematics. Turing-complete. Independent of any database. |
A knot database — stores presentations, invariants, fingerprints, equivalence classes and witnesses. |
|
QuandleDB’s resolution language, developed jointly with it. Specified in the
|
|
Important
|
Earlier revisions of this README were titled "Tangle / KRL" and described
Tangle as the substrate of a
The projects remain related by domain and are developed by the same author; what is removed here is a claimed architectural dependency that does not exist. |
A core fragment of the language is formalised and mechanised in Lean 4.
Verified on 2026-07-21 by running the repository’s own oracle,
cd proofs && lean Tangle.lean — exit 0, no errors:
| Property | Status |
|---|---|
|
proved |
|
proved |
|
proved |
|
proved |
Decidability of type checking ( |
proved |
The proofs are self-contained (no Mathlib dependency) and contain zero uses of
sorry and zero axiom declarations across 2,128 lines — so "builds" and
"proved" mean the same thing here, which is not automatic.
They cover echo types: structured loss as a type-system feature. close
(braid closure) is the canonical lossy map, and echoClose/lower/residue
make that loss recoverable at the type level — a simply-typed shadow of
echo-types. All four safety
theorems cover them.
See proofs/Tangle.lean, proofs/README.md, docs/spec/FORMAL-SEMANTICS.md,
and PROOF-NARRATIVE.md / PROOF-NEEDS.md.
This formal core covers the structural heart of the language, though not all surface features.
Tangle’s breadth is expressed as dialects, each with its own grammar sketch
under dialects/:
-
braid-calculus— braid words and their relations -
skein-algebra— skein relations and invariant computation -
string-diagram— monoidal-category string diagrams -
virtual-knot— virtual knot theory -
quantum-circuit— circuits as topological objects
Tangle is an active research system. Read it as a formally grounded core with an evolving implementation around it.
| Area | State |
|---|---|
Lean 4 formal core |
Verified — see above |
Grammars |
|
OCaml compiler ( |
Lexer, parser, AST, typechecker, evaluator, pretty-printer, REPL, braid equivalence, plus LSP and WASM targets. Not built by CI |
Rust / Zig components |
18 |
Database integration |
Not implemented |
|
Note
|
Only the Lean proofs are gated by CI ( |
-
richer categorical abstractions
-
optimisation via equivalence classes
-
alternative evaluation models based on rewriting
These are not yet stable features.
-
proofs/Tangle.lean— mechanised type-safety proof (the load-bearing artefact) -
docs/spec/FORMAL-SEMANTICS.md— formal model -
src/tangle.ebnf— surface grammar -
dialects/— the breadth of the language -
compiler/lib/— the OCaml front end