diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml index 13327b9..3f783fa 100644 --- a/.github/workflows/governance.yml +++ b/.github/workflows/governance.yml @@ -13,4 +13,4 @@ permissions: jobs: governance: - uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@d7c22711e830e1f383846472f6e9b99debdb201e \ No newline at end of file + uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@f9dca6ded2cad8ab54044c1cb0489b558ae2682b \ No newline at end of file diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index 02b0e9c..42fed59 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.github/workflows/hypatia-scan.yml @@ -12,8 +12,11 @@ on: permissions: contents: read - security-events: read + # The reusable declares security-events: write (it uploads SARIF). A called + # workflow cannot escalate beyond the caller's grant, so `read` here makes the + # whole run a startup_failure with zero jobs and no log. + security-events: write jobs: scan: - uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@d7c22711e830e1f383846472f6e9b99debdb201e \ No newline at end of file + uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@f9dca6ded2cad8ab54044c1cb0489b558ae2682b \ No newline at end of file diff --git a/.github/workflows/jekyll-gh-pages.yml b/.github/workflows/jekyll-gh-pages.yml deleted file mode 100644 index cd05ddc..0000000 --- a/.github/workflows/jekyll-gh-pages.yml +++ /dev/null @@ -1,48 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# Sample workflow for building and deploying a Jekyll site to GitHub Pages -name: Deploy Jekyll with GitHub Pages dependencies preinstalled -on: - # Runs on pushes targeting the default branch - push: - branches: ["main"] - # Allows you to run this workflow manually from the Actions tab - workflow_dispatch: -# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages -permissions: - contents: read - pages: write - id-token: write -# Allow only one concurrent deployment, skipping runs queued between the run in-progress and latest queued. -# However, do NOT cancel in-progress runs as we want to allow these production deployments to complete. -concurrency: - group: "pages" - cancel-in-progress: false -jobs: - # Build job - build: - runs-on: ubuntu-latest - timeout-minutes: 15 - steps: - - name: Checkout - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 - - name: Setup Pages - uses: actions/configure-pages@45bfe0192ca1faeb007ade9deae92b16b8254a0d # v6.0.0 - - name: Build with Jekyll - uses: actions/jekyll-build-pages@44a6e6beabd48582f863aeeb6cb2151cc1716697 # v1 - with: - source: ./ - destination: ./_site - - name: Upload artifact - uses: actions/upload-pages-artifact@fc324d3547104276b827a68afc52ff2a11cc49c9 # v4 - # Deployment job - deploy: - environment: - name: github-pages - url: ${{ steps.deployment.outputs.page_url }} - runs-on: ubuntu-latest - timeout-minutes: 15 - needs: build - steps: - - name: Deploy to GitHub Pages - id: deployment - uses: actions/deploy-pages@cd2ce8fcbc39b97be8ca5fce6e763baed58fa128 # v5.0.0 diff --git a/.github/workflows/jekyll.yml b/.github/workflows/jekyll.yml deleted file mode 100644 index f097625..0000000 --- a/.github/workflows/jekyll.yml +++ /dev/null @@ -1,62 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# This workflow uses actions that are not certified by GitHub. -# They are provided by a third-party and are governed by -# separate terms of service, privacy policy, and support -# documentation. - -# Sample workflow for building and deploying a Jekyll site to GitHub Pages -name: Deploy Jekyll site to Pages -on: - # Runs on pushes targeting the default branch - push: - branches: ["main"] - # Allows you to run this workflow manually from the Actions tab - workflow_dispatch: -# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages -permissions: - contents: read - pages: write - id-token: write -# Allow only one concurrent deployment, skipping runs queued between the run in-progress and latest queued. -# However, do NOT cancel in-progress runs as we want to allow these production deployments to complete. -concurrency: - group: "pages" - cancel-in-progress: false -jobs: - # Build job - build: - runs-on: ubuntu-latest - timeout-minutes: 15 - steps: - - name: Checkout - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 - - name: Setup Ruby - # https://github.com/ruby/setup-ruby/releases/tag/v1.207.0 - uses: ruby/setup-ruby@003a5c4d8d6321bd302e38f6f0ec593f77f06600 - with: - ruby-version: '3.1' # Not needed with a .ruby-version file - bundler-cache: true # runs 'bundle install' and caches installed gems automatically - cache-version: 0 # Increment this number if you need to re-download cached gems - - name: Setup Pages - id: pages - uses: actions/configure-pages@45bfe0192ca1faeb007ade9deae92b16b8254a0d # v6.0.0 - - name: Build with Jekyll - # Outputs to the './_site' directory by default - run: bundle exec jekyll build --baseurl "${{ steps.pages.outputs.base_path }}" - env: - JEKYLL_ENV: production - - name: Upload artifact - # Automatically uploads an artifact from the './_site' directory by default - uses: actions/upload-pages-artifact@fc324d3547104276b827a68afc52ff2a11cc49c9 # v4 - # Deployment job - deploy: - environment: - name: github-pages - url: ${{ steps.deployment.outputs.page_url }} - runs-on: ubuntu-latest - timeout-minutes: 15 - needs: build - steps: - - name: Deploy to GitHub Pages - id: deployment - uses: actions/deploy-pages@cd2ce8fcbc39b97be8ca5fce6e763baed58fa128 # v5.0.0 diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml index f95bced..b3d9333 100644 --- a/.github/workflows/pages.yml +++ b/.github/workflows/pages.yml @@ -1,3 +1,5 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) name: GitHub Pages (Ddraig SSG) on: push: @@ -18,9 +20,9 @@ jobs: image: ghcr.io/stefan-hoeck/idris2-pack@sha256:f0758996a931fb35d9ecb1de273c4d59dabe2a09b433afc7e357f65a08b7e1ff steps: - name: Checkout Site - uses: actions/checkout@v7 + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 - name: Checkout Ddraig SSG - uses: actions/checkout@v7 + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 with: repository: hyperpolymath/ddraig-ssg path: .ddraig-ssg @@ -37,7 +39,7 @@ jobs: fi ./.ddraig-ssg/build/exec/ddraig build src _site https://hyperpolymath.github.io/${GITHUB_REPOSITORY#*/} - name: Upload artifact - uses: actions/upload-pages-artifact@v5 + uses: actions/upload-pages-artifact@fc324d3547104276b827a68afc52ff2a11cc49c9 # v5 with: path: '_site' deploy: @@ -50,4 +52,4 @@ jobs: steps: - name: Deploy to GitHub Pages id: deployment - uses: actions/deploy-pages@v5 + uses: actions/deploy-pages@cd2ce8fcbc39b97be8ca5fce6e763baed58fa128 # v5 diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml index 4ecc2ad..db25ae8 100644 --- a/.github/workflows/scorecard.yml +++ b/.github/workflows/scorecard.yml @@ -13,7 +13,7 @@ permissions: jobs: scorecard: - uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@d7c22711e830e1f383846472f6e9b99debdb201e + uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@f9dca6ded2cad8ab54044c1cb0489b558ae2682b permissions: contents: read security-events: write diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index 265e72b..8b4dec1 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -220,3 +220,67 @@ un-run toolchains stated rather than implied. `-S`; the signed git commit over this content, at the SHA above, is the authoritative form. * *Signed-off-date:* (fill on signing) + +''' + +== Erratum — 2026-07-21 + +This section corrects the affirmation above. The original text is left intact: +an affirmation is a dated claim about a past state, and amending it in place +would falsify a record. Two of its claims have since been shown to be wrong, +and one of its acknowledged gaps has since been closed. + +=== Correction 1 — the stack does not exist + +The affirmation records, as *maintainer-confirmed*, the ladder: + +[literal] +KRL -> TangleIR -> VerisimCore -> Skein/QuandleDB + +`TangleIR` does not exist. The identifier appears in *no source file* in this +repository (0 hits across `.rs`, `.zig` and `.lean`) and in *no source file* in +the KRL implementation at `quandledb/server/krl/`. It existed only in prose, in +both repositories, and has been removed from `README.adoc`. + +Nor is KRL a surface language for Tangle. KRL is QuandleDB's resolution +language, developed jointly with QuandleDB; it neither compiles to nor depends +on Tangle. The three projects share a subject matter, not an architecture. + +The confirmation recorded on 2026-06-19 was a confirmation of the README's +diagram, and that diagram was wrong. Nothing here suggests bad faith — the +affirmation is careful, and states plainly which of its checks were not run. + +=== Correction 2 — the "one-line characterisation" should not be quoted as-is + +The characterisation invites quotation. It should not be quoted while it +describes Tangle as "the proven type-safe small-step core + TangleIR of the KRL +stack". Everything else in that sentence survives: the OCaml compiler, the Rust +LSP/WASM targets, the Lean 4 proofs and the five dialects are all real. + +=== Discharge — the Lean proofs have now been run + +The affirmation states: *"OCaml + Lean not run (absent)"*, and concludes that +*"structure + the repo's proof records are confirmed, not a fresh green build"*. + +That gap is now closed for Lean. On 2026-07-21 the repository's own documented +oracle was executed: + +[source,console] +---- +$ cd proofs && lean Tangle.lean +$ echo $? +0 +---- + +Exit 0, no errors, using the pinned toolchain from `proofs/lean-toolchain` +(`leanprover/lean4:v4.14.0`). The proofs are self-contained — `Tangle.lean` has +no `import` lines at all, so no Mathlib — and contain *zero* occurrences of +`sorry` and *zero* `axiom` declarations across 2,128 lines. `progress`, +`preservation`, `determinism`, `type_safety`, `infer_sound`, `infer_complete` +and `infer_iff_hasType` are all present with real proof terms. + +This matters because "the Lean build is green" and "the theorems are proved" are +not the same claim in general: an `axiom` stub compiles cleanly while proving +nothing. Here they coincide, and that was checked rather than assumed. + +The OCaml compiler remains unbuilt — no workflow in this repository builds it. diff --git a/READINESS.md b/READINESS.md index 699ec03..c150e38 100644 --- a/READINESS.md +++ b/READINESS.md @@ -6,45 +6,116 @@ Copyright (c) Jonathan D.A. Jewell # Component Readiness — Tangle (language) -**Current Grade:** C -**Assessed:** 2026-04-05 +**Current Grade:** D +**Assessed:** 2026-07-21 (demoted C → D) **Standard:** [CRG v2.0 STRICT](../standards/component-readiness-grades/) -## Grade rationale (evidence for C) +## Why the grade moved C → D -Works reliably on own project + annotated. Tangle is a Turing-complete -topological programming language with a compiler, LSP, and wasm backend. +Grade C means *self-validated in the home context*; the D → C promotion trigger +is *"dogfood it hard in the home context."* The previous assessment cited +exactly one piece of dogfooding evidence: -### Evidence +> **Dogfooding:** Used internally as host for the KRL (Knot Resolution Language) DSL -- **Tests:** 6 dune test suites (parser, typecheck, eval, e2e, property, compositional) -- **Annotation:** 8 per-directory READMEs across compiler/, lib/, examples/, docs/ -- **Dogfooding:** Used internally as host for the KRL (Knot Resolution Language) DSL -- **RSR compliance:** 0-AI-MANIFEST.a2ml, `.machine_readable/6a2/`, 14+ workflows, SECURITY/CONTRIBUTING/CODE_OF_CONDUCT, EXPLAINME.adoc, TEST-NEEDS.md, PROOF-NEEDS.md -- **Formal proofs:** Lean 4 proofs for progress, preservation, determinism -- **WASM backend:** Compositional PD compiler with wasm codegen -- **CI:** Clean; panic-attack assail 0 findings +**That is not true.** KRL is not built on Tangle. KRL is QuandleDB's resolution +language, developed jointly with QuandleDB; it neither compiles to nor depends +on Tangle, and the `TangleIR` layer that was supposed to connect them does not +exist in any source file in either repository. See the erratum in +`AFFIRMATION.adoc`. + +With that claim withdrawn there is no dogfooding evidence, so C is not +supported. Two further corrections to the previous assessment: + +- **"CI: Clean" was false.** At the time of this assessment `main` was failing + Governance and both Jekyll Pages workflows. +- **The test suites are not run by CI.** Eight OCaml test files exist under + `compiler/test/`, but no workflow in this repository invokes `dune` or + `cargo test`. Their passing state is unverified by this repository's own CI. + +This is a correction to the record, not a regression in the work. The formal +core in particular got *stronger* this cycle — see below. + +--- + +## Grade rationale (evidence for D) + +Grade D: *"works on some inputs, some cases, or some configurations, but not +systematically … either needs to be narrowed in scope so that its documented +capabilities match its actual capabilities, or needs the inconsistencies +fixed."* Narrowing the documented scope is exactly what this revision does. + +### Verified evidence + +| Artefact | Check | Result | +|---|---|---| +| `proofs/Tangle.lean` | `cd proofs && lean Tangle.lean` (the repo's own documented oracle) | **exit 0, no errors** | +| `proofs/Tangle.lean` | `sorry` count | **0** | +| `proofs/Tangle.lean` | `axiom` count | **0** | +| Theorems | `progress`, `preservation`, `determinism`, `type_safety`, `infer_sound`, `infer_complete`, `infer_iff_hasType` | all present with real proof terms | +| Dependencies | `import` lines in `Tangle.lean` | **0** — self-contained, no Mathlib | + +Run on 2026-07-21 with the pinned toolchain (`leanprover/lean4:v4.14.0`). This +is worth stating precisely: a Lean file full of `axiom` stubs compiles cleanly +while proving nothing, so "the build is green" and "the theorems are proved" are +different claims. Here they coincide, and that was checked. + +### Present but unverified + +- **OCaml compiler** (`compiler/`) — lexer, parser, AST, typechecker, evaluator, + pretty-printer, REPL, braid equivalence, LSP and WASM targets. Not built by + any workflow. +- **Test suites** — 8 files under `compiler/test/` (`test_parser`, + `test_typecheck`, `test_eval`, `test_e2e`, `test_property`, + `test_compositional`, `test_check`, `test_roundtrip`) plus `tg3`/`tg5`/`tg7`/ + `tg8` directories. Not run by any workflow. +- **Rust / Zig components** — 18 `.rs`, 3 `.zig`. Not built by any workflow. +- **Five dialects** — grammar sketches only. + +### Structural evidence + +- Per-directory README annotation across `compiler/`, `dialects/`, `docs/`. +- RSR compliance: `0-AI-MANIFEST.a2ml`, `.machine_readable/6a2/`, workflows, + SECURITY / CONTRIBUTING / CODE_OF_CONDUCT, `EXPLAINME.adoc`, `TEST-NEEDS.md`, + `PROOF-NEEDS.md`. + +--- ## Gaps preventing higher grades +### Blocks C (self-validated in the home context) + +1. **No CI gate on the implementation.** The OCaml compiler, its 8 test suites, + and the Rust and Zig components are not built or run by any workflow. Until + they are, "works reliably" is not an evidenced claim. This is the single + highest-value fix available to this repository. +2. **No dogfooding.** Nothing is currently built on Tangle. The previous claim + to the contrary was false. + ### Blocks B (6+ diverse external targets) + - No external language users outside hyperpolymath. -- KRL is the only DSL built on Tangle so far — need 5 more distinct domain DSLs - to demonstrate the host-language claim. - No external submissions to language research venues confirming the phase separation or compositional PD model. ### Blocks A + - Requires B first. -## What to do for B +--- + +## What to do next -1. Build 5 more DSLs on top of Tangle (not just KRL) — e.g. a braid-group - calculus, a category-theory calculus, a quantum-circuit calculus. -2. Get external feedback on the surface syntax and compiler from language - researchers. -3. Track the 6 targets here. +1. **Add a workflow that runs `dune build && dune test`.** Eight test suites + already exist; nothing executes them. This is the cheapest available uplift + and is a precondition for any claim above D. +2. Add a workflow that builds the Rust and Zig components. +3. Build something real on Tangle, in its own right — a braid-group calculus, a + category-theory calculus, a quantum-circuit calculus. The five dialects are + the natural candidates and currently exist only as grammar sketches. + Note that this must be genuine dogfooding of *Tangle*; KRL does not count and + never did. ## Review cycle -Reassess per release. Next review: on any compiler/LSP/wasm behavioural change. +Reassess when the compiler is built and its tests are run by CI. diff --git a/README.adoc b/README.adoc index bcb98df..9b2ad85 100644 --- a/README.adoc +++ b/README.adoc @@ -2,37 +2,39 @@ // Copyright (c) Jonathan D.A. Jewell // SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell -= Tangle / KRL — Topological Programming Language += Tangle — a general language for knot mathematics image:https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity[OpenSSF Best Practices,link="https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/tangle"] image:https://img.shields.io/badge/License-MPL_2.0-blue.svg[License: MPL-2.0,link="https://opensource.org/licenses/MPL-2.0"] image:https://api.thegreenwebfoundation.org/greencheckimage/github.com[Green Web,link="https://www.thegreenwebfoundation.org/green-web-check/?url=github.com"] -A research language exploring *computation as topology*, where programs are structured objects and equivalence is defined by transformation. +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. --- == Overview -Tangle (via KRL — Knot Resolution Language) is an experimental programming language in which: +Tangle is an experimental, Turing-complete programming language in which: -> *programs are structured as tangles (braids), and program equivalence is defined by isotopy.* +> *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*. +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. -This allows reasoning about programs in terms of: - -* structure -* equivalence under transformation -* 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. --- -== Core Idea - -The central idea of Tangle is: +== Core idea -> *computation is construction of structured objects, and meaning is preserved under valid transformations.* +> *computation is construction of structured objects, and meaning is preserved +> under valid transformations.* In this setting: @@ -40,140 +42,148 @@ In this setting: * 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) -* algebraic invariants (classification via structure) +This aligns with concepts from knot theory (Reidemeister moves), category theory +(morphisms and composition), and algebraic invariants (classification via +structure). --- -== KRL — Knot Resolution Language - -KRL is the surface language used to interact with the system — a *resolution DSL*, -*not merely* a query language. +== Relationship to KRL and QuandleDB -It is organised around four fundamental operations: +Tangle is a *separate project* from KRL and QuandleDB. The three share a subject +matter, not an architecture. [cols="1,3"] |=== -|Operation |Role +|Project |What it is -|Construct -|Create or declare presentations, structures, claims, datasets +|*Tangle* (this repository) +|A general language for knot mathematics. Turing-complete. Independent of any + database. -|Transform -|Rewrite, normalize, compose, concatenate, permute, mutate +|https://github.com/hyperpolymath/quandledb[*QuandleDB*] +|A knot database — stores presentations, invariants, fingerprints, equivalence + classes and witnesses. -|Resolve -|Decide / disambiguate / evaluate equivalence or identity questions - -|Retrieve -|Inspect, fetch, project, explain, or return stored/computed results +|https://github.com/hyperpolymath/krl[*KRL*] +|QuandleDB's resolution language, developed jointly with it. Specified in the + `krl` repository, implemented in `quandledb/server/krl/`. |=== -KRL is not a general-purpose language; it is a *domain language for structured -objects and their equivalence*. *Retrieve* recovers resolution-relevant artefacts -(presentations, invariants, witnesses, equivalence classes, prior resolutions, -explanations, provenance) — it is *not* arbitrary database querying. See krl -`docs/decisions/0002-query-language-deferred.adoc`. - ---- +[IMPORTANT] +==== +Earlier revisions of this README were titled *"Tangle / KRL"* and described +Tangle as the substrate of a `KRL -> TangleIR -> Tangle core -> QuandleDB` +stack. That was wrong on both counts. -== Architecture +* KRL is not Tangle's surface language. It is QuandleDB's, and it neither + compiles to nor depends on Tangle. +* There is no `TangleIR`. The identifier appears in *no source file* in this + repository, nor in the KRL implementation — it existed only in prose. -Tangle is part of a layered system: +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. +==== --- -KRL (surface language — resolution DSL, not merely a query language) -↓ -TangleIR (canonical interchange representation) -↓ -Tangle core (this repo — proven type-safe small-step semantics) -↓ -QuandleDB + Skein.jl (persistence + invariant/equivalence; computational engine) -------------------------------------------- +== Formal core -* *TangleIR* is the central representation shared across layers -* other components provide views, transformations, or storage +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: -== Formal Core +[cols="2,1"] +|=== +|Property |Status + +|`progress` +|proved -A core fragment of the language has been formalised and mechanised. +|`preservation` +|proved -This includes: +|`determinism` +|proved -* a typed core language (braid words, composition, tensor) -* small-step operational semantics -* mechanised proofs in Lean 4: +|`type_safety` +|proved - * progress - * preservation - * determinism - * type safety - * decidability of type checking (`infer` ≡ `HasType`) +|Decidability of type checking (`infer` == `HasType`) +|proved +|=== -* *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 - hyperpolymath/echo-types). All four safety theorems cover them. +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. -See: +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 +https://github.com/hyperpolymath/echo-types[echo-types]. All four safety +theorems cover them. -* `proofs/Tangle.lean` (and `proofs/README.md` to build/verify) -* `docs/spec/FORMAL-SEMANTICS.md` -* `PROOF-NARRATIVE.md` / `PROOF-NEEDS.md` +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. +This formal core covers the structural heart of the language, though not all +surface features. --- -== Current Status +== Dialects -Tangle/KRL is an *active research system*. +Tangle's breadth is expressed as dialects, each with its own grammar sketch +under `dialects/`: -At present: +* `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 -* grammar is defined (EBNF / PEG in progress) -* AST and type system are partially implemented -* compiler pipeline (AST → TangleIR) is in development -* decompilation (IR → source) is incomplete -* database integration (Skein / QuandleDB) is planned or partial +--- -It should be read as: +== Current status -> a formally grounded core with an evolving implementation and surrounding research system. +Tangle is an active research system. Read it as *a formally grounded core with +an evolving implementation around it*. ---- +[cols="1,2"] +|=== +|Area |State -== Scope +|Lean 4 formal core +|Verified — see above -=== Implemented / Grounded +|Grammars +|`src/tangle.ebnf`, `src/tangle-jtv.ebnf`, `spec/grammar.ebnf`, plus five + dialect sketches -* core grammar (defined) -* AST and type structure -* Lean formalisation of core fragment -* partial compiler pipeline -* example programs +|OCaml compiler (`compiler/`) +|Lexer, parser, AST, typechecker, evaluator, pretty-printer, REPL, braid + equivalence, plus LSP and WASM targets. *Not built by CI* ---- +|Rust / Zig components +|18 `.rs`, 3 `.zig`. *Not built by CI* -=== In Progress +|Database integration +|Not implemented +|=== -* parser and full compiler -* IR integration across components -* equivalence resolution via QuandleDB -* invariant-based querying +[NOTE] +==== +Only the Lean proofs are gated by CI (`.github/workflows/lean-proofs.yml`). +The OCaml compiler, the Rust components and the Zig components are not built by +any workflow, so their state is unverified by this repository's own CI. +==== --- -=== Research Directions +== Research directions * richer categorical abstractions -* deeper integration with algebraic databases * optimisation via equivalence classes * alternative evaluation models based on rewriting @@ -181,36 +191,15 @@ These are not yet stable features. --- -== Relationship to Other Projects - -Tangle is closely connected to: - -* *QuandleDB* — equivalence and classification via algebraic invariants -* *Skein.jl* — persistence and indexing of structured objects -* *Nextgen Languages* — broader research context - ---- - -== How to Read This Repository - -Recommended entry points: +== How to read this repository -* `Tangle.lean` — mechanised type safety proof +* `proofs/Tangle.lean` — mechanised type-safety proof (the load-bearing artefact) * `docs/spec/FORMAL-SEMANTICS.md` — formal model -* grammar files (`src/tangle.ebnf` or equivalent) -* examples demonstrating composition and transformation - ---- - -== Summary - -Tangle/KRL is best understood as: - -> a research language that treats programs as structured objects, with meaning defined by transformation and equivalence, supported by a partially mechanised formal core and an evolving implementation. - - -== License +* `src/tangle.ebnf` — surface grammar +* `dialects/` — the breadth of the language +* `compiler/lib/` — the OCaml front end -This project is licensed under the Mozilla Public License, v. 2.0. See the `LICENSE` file for details. +== Licence -SPDX-License-Identifier: CC-BY-SA-4.0 +This project is licensed under the Mozilla Public License, v. 2.0. See the +`LICENSE` file for details. This document is CC-BY-SA-4.0. diff --git a/dialects/README.md b/dialects/README.md index 62a5641..1cc271e 100644 --- a/dialects/README.md +++ b/dialects/README.md @@ -15,23 +15,27 @@ coherent and could be built out, not a complete implementation. ## The pattern -When a DSL matures from sketch → alpha implementation, it should follow -the KRL precedent: +When a DSL matures from sketch → alpha implementation: 1. Start with an EBNF grammar sketch here (`grammar-sketch.ebnf`) 2. Write 1-3 example programs -3. When ready to implement: graduate to its own top-level repo (like `krl/`) -4. Implement parser in Tangle OCaml or sibling language -5. Wire through to TangleIR or its own IR type +3. When ready to implement, decide whether it stays in-tree or graduates to + its own repository +4. Implement the parser in Tangle's OCaml front end or a sibling language +5. Define its IR type -Keeping sketches here demonstrates Tangle's claim to be a general -multi-DSL host, not a single-purpose language. +No dialect has yet made this journey, so there is no precedent to follow — +these are all still at step 1. + +These sketches set out what a general multi-DSL host *would* cover. They do not +yet evidence the claim: nothing here is implemented, and nothing is currently +built on Tangle. Implementing one of them end to end is what would turn the +claim into evidence. ## Current scaffolds | Dialect | Status | Domain | |---|---|---| -| [krl](../../krl/) (separate repo) | grade E → D (v0.2 parser 2026-04-12) | Knot resolution — construct, transform, resolve, retrieve | | [braid-calculus](braid-calculus/) | sketch | Artin braid group Bn calculus | | [quantum-circuit](quantum-circuit/) | sketch | Quantum circuit compositional calculus | | [string-diagram](string-diagram/) | sketch | Monoidal/braided category string diagrams | @@ -40,10 +44,18 @@ multi-DSL host, not a single-purpose language. ## Relationship to KRL -KRL lives at `/var/mnt/eclipse/repos/krl` (sibling top-level repo), NOT -here. This is intentional: KRL has graduated past the scaffold stage and -earned its own repo. These scaffolds represent future candidates that -may graduate similarly. +**KRL is not a Tangle dialect and never was.** It was previously listed here as +one that had "graduated" to its own repository; that was part of a wider +conflation of the two projects, corrected in `README.adoc` and in the erratum to +`AFFIRMATION.adoc`. + +KRL is the resolution language for +[QuandleDB](https://github.com/hyperpolymath/quandledb), developed jointly with +it, and lives at [hyperpolymath/krl](https://github.com/hyperpolymath/krl). It +does not compile to, lower into, or otherwise depend on Tangle. The two share a +subject matter, not an architecture. + +The scaffolds listed above are Tangle's own dialects. ## Contribution