This category contains programming and specification languages built on formal foundations: type theory, category theory, knot theory, and domain-specific algebraic structures.
Each language is designed around a specific set of guarantees that existing languages cannot provide — not as extensions, but as structural properties.
Surface language for constructing, transforming, resolving, and retrieving topological objects (tangles, knots, links).
KRL spans four operations grounded in knot theory:
-
Construct — compositional tangle building (Tangle PL compiler module)
-
Transform — Reidemeister-style rewriting (KnotTheory.jl engine)
-
Resolve — isotopy equivalence and quandle-based classification (QuandleDB)
-
Retrieve — invariant-indexed query (Skein.jl)
Phase-separated language: Turing-complete development phase, Turing-incomplete deployment phase. Targets secure edge/IoT environments. EBNF v0.6 complete; formal proofs in progress.
Economics-as-Code. Resource constraints as first-class language citizens. EBNF finalised. Targets formally verified resource allocation systems.
Hard real-time systems language. Dependent, session, and linear types. DO-178C alignment. Zig compiler recommended.
Four-dialect language family. Me: playground (ReScript). Solo: OCaml compiler ~60%. Duet/Ensemble: specified.
-
Every language targets a class of structural guarantees, not just features
-
Formal semantics before implementation
-
Compiler targets are canonical IRs, not direct code generation
-
Each language pairs with a database or verification system in
nextgen-databases
The most developed system in this category is the KRL stack:
KRL surface syntax ↓ compiled by TanglePL module TangleIR (canonical interchange) ↓ abstracted by VerisimCore VerisimMorphism (categorical view) ↓ persisted by Skein.jl ↓ fingerprinted by QuandleDB
TangleIR is the spine. Everything else is a view over it or a service to it.
| Language | Status | Notes |
|---|---|---|
KRL / Tangle PL |
Active — compiler in progress |
Grammar defined; AST → IR compiler in development |
Oblíbený |
Active — EBNF stable |
Formal proofs and BOINC verification planned |
Eclexia |
Specified |
EBNF finalised; implementation not started |
Betlang |
Specified |
Compiler not started; Zig recommended |
Phronesis |
Active — early |
40-line EBNF; IRTF submission planned |
My Language |
Active — Solo 60% |
Me dialect working; Solo OCaml compiler in progress |
JtV |
Design phase |
Architecture specified |