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

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.

---

Haec

A Turing-complete language whose type discipline is trope-particularity: every operation on a property-instance carries a graded loss-shape, lowered to a language-neutral Trope IR and checked against a declared use-model by a separate, portable checker (hyperpolymath/trope-checker, an Idris2 verified core plus an executable). The named effects, residual, and verdict live in hyperpolymath/trope-particularity-workbench. Shares the loss-with-residue substrate with echo-types.

Status: design (grammar + elaboration + round-tripping examples); the checker’s verified core typechecks with no axioms.

---

KitchenSpeak (experimental DSL — moved out)

An experimental, formally-verified orchestration DSL for the domestic kitchen, used as a teaching vehicle for advanced type theory. It is no longer carried in this coordinator: its canonical home is the standalone hyperpolymath/kitchenspeak repository — v2.0 puts physics in the types (so curdle / scorch / bake-the-spatula / over-torque are compile errors), with a reference OCaml compiler and machine-checked Agda proofs.

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 where identity, provenance, or equivalence matter Type-theoretic boundaries are made explicit: total proof-like fragments are distinguished from partial or Turing-complete execution fragments

Relationship to Databases

These languages are designed to work with systems that treat equivalence, provenance, and semantic identity as first-class concepts:

KRL ↔ QuandleDB / Skein JtV ↔ future equivalence-aware runtime and storage models

See the nextgen-databases repository for details.

WasmGC Compilation Infrastructure

Several languages in this family (AffineScript, Ephapax) compile to typed WebAssembly (WasmGC). Their shared compilation target and binary convention infrastructure lives in a separate repository:

• typed-wasm — TypeLL progressive type safety for WasmGC linear memory, and the aggregate library that defines shared type layout and ABI conventions for WasmGC-targeting languages. AffineScript and Ephapax reference typed-wasm as their binary convergence point.

typed-wasm is not a language in the nextgen-languages sense — it is a compilation target and a library. It lives in `nextgen-typing’s scope (the type theory pipeline) but is documented here for discoverability.

See also: * hyperpolymath/affinescript — affine type discipline, compiles to WasmGC * hyperpolymath/ephapax — dyadic linear/affine type system, compiles to WasmGC

Shared Formal Substrate — echo-types

Several languages here reason about irreversible transformation with retained residue — an egg cannot be uncracked, flour and water become dough. The formal account of that idea lives in a separate repository:

• echo-types — a constructive Agda library for Echo types: the proof-relevant residue of structured (non-total) loss, Echo f y := Σ (x : A), f x ≡ y. Its EchoTypes.jl companion is an executable finite-domain model.

KitchenSpeak is the first consumer: per ADR 0004 its Echo type attaches to the Linear/Dyadic consumption types (where irreversible transformation and provenance live), with echo-types as the substrate. echo-types is not a language in the nextgen-languages sense — it is a shared formal library.

Status

This repository should be read as a research-exploration coordinator rather than a production system. The work it tracks spans, across the individual language repos:

• formal proofs (e.g. the Tangle core)

• partial compilers and grammars

• design documents and specifications

Suggested Entry Points

Each language lives in its own hyperpolymath/<lang> repo; start there. For orientation:

• hyperpolymath/tangle — Tangle.lean, the mechanised type-safety proof for the Tangle (KRL) core; topological language design

• hyperpolymath/jtv — computation as path-based construction

Pedagogy and Learner Materials

Teaching and learning materials for the languages in this family are not hosted in this repo. They live in two distinct layers:

• Curriculum source of truth — tentacles-agentic-syllabus (top-level repo; previously hyperpolymath/7-tentacles). This is the aspect-agent-driven curriculum framework that defines the syllabus, the agents, the kin framework, and the (to-be-built) Me runtime projector that generates per-learner, per-task scoped views over the real language. Me is not a fourth dialect of any language here — it is an on-the-fly projection over whichever base dialect a learner picks, produced from an A2ML task spec by the aspect-agents.

• Per-language applied layers — my-lang’s applied learner & teacher materials live in my-lang/frontier-practices/ (previously my-lang/7-tentacles/). This parallels the pattern of ~/Desktop/Frontier_Programming_Practices_AffineScript/ for AffineScript. Other languages may grow their own frontier-practices/ subdirectories as their applied learning surface matures.

This coordinator points at the language implementations — compilers, grammars, type systems, semantics — which live in each hyperpolymath/<lang> repo, not here. If you are looking for lessons, exercises, worked examples, or curriculum content, start in tentacles-agentic-syllabus and the relevant language’s frontier-practices/ directory.

Historical Note — Me Pivot

A standalone exploratory attempt to build Me as a static dialect compiler (hyperpolymath/me-dialect on GitHub) has been archived. The earlier in-tree scaffolding at my-lang/dialects/me/ has been sidelined to my-lang/_exploratory/me-scaffolding/. See that directory’s SIDELINED.adoc and the tentacles-agentic-syllabus/me/README.adoc design document for the architectural pivot: Me is an agent-generated runtime projection, not a static dialect compiler.