Next-Generation Languages — Research Overview

Overview

This repository contains exploratory work on a family of programming and specification languages built around a shared principle:

computation and meaning are determined by structured equivalence, not just raw values.

Across different domains (topology, resource systems, ethics, computation), these languages investigate how formal guarantees can be built into the structure of a language itself rather than added as tooling or conventions.

This is research-stage work: some components are partially implemented or formally specified, others remain conceptual.

Core Idea

The central idea underlying these languages is:

identity is defined by equivalence under transformation.

This appears in different forms:

• Computation: values arise from construction paths, and meaning depends on those paths

• Topology: objects are equivalent under isotopy (continuous deformation)

• Type systems: structure constrains what transformations are valid

• Execution: guarantees (termination, purity, resource bounds) are encoded in the language design

These languages explore different instances of this idea.

Projects

JtV — Julia the Viper

A foundational language exploring computation as additive construction from neutral anchors (CNO).

• Identity is determined by equivalence of construction paths

• Inversion is treated as retraction of construction, not primitive subtraction

• Strong separation between data and control (Harvard-style architecture)

Status: design-stage, with partial specifications and experimental implementations.

---

KRL — Knot Resolution Language (Tangle)

A topologically inspired language where programs are represented as tangles (braids), and equivalence is defined by isotopy.

• Composition and tensor operations correspond to braid structure

• Formal semantics specified

• Core type system mechanised in Lean (see Tangle.lean)

Status: compiler and tooling in progress; formal core partially verified.

---

Oblíbený

A phase-separated language with:

• Turing-complete development phase

• Turing-incomplete deployment phase

Designed for secure and constrained environments.

Status: grammar stable; formal verification in progress.

---

Eclexia

An “economics-as-code” language where resource constraints are first-class.

Status: specified; implementation not started.

---

Betlang

A language for hard real-time systems using dependent, session, and linear types.

Status: specified.

---

Phronesis

A domain-specific language for expressing ethical constraints in multi-agent systems.

Status: early-stage.

---

My Language (Me / Solo / Duet / Ensemble)

A multi-dialect experimental language family exploring different levels of abstraction and composition.

Status: partially implemented.

Common Principles

Across these languages:

• Formal semantics precede implementation

• Each language targets a specific structural guarantee

• Canonical intermediate representations (IRs) are preferred over direct compilation

• Languages are paired with database or verification systems (see nextgen-databases)

Relationship to Databases

These languages are designed to work with systems that treat equivalence as a first-class concept:

• KRL ↔ QuandleDB / Skein

• JtV ↔ future equivalence-aware runtime and storage models

See the nextgen-databases repository for details.

Status

This repository should be read as a research exploration rather than a production system.

Some components include:

• formal proofs (e.g. Tangle core)

• partial compilers and grammars

• design documents and specifications

Suggested Entry Points

• Tangle.lean — mechanised type safety proof for the Tangle core

• KRL / Tangle documentation — topological language design

• JtV documentation — emerging model of computation as path-based construction