diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc new file mode 100644 index 0000000..b6ba823 --- /dev/null +++ b/CHANGELOG.adoc @@ -0,0 +1,95 @@ +== Changelog + +All notable changes to the nextgen-languages parent repository. + +=== 2026-06-12 + +==== Changed + +* _KitchenSpeak Echo bridge is now MACHINE-CHECKED against the real +`+hyperpolymath/echo-types+` library._ +`+kitchenspeak/proofs/agda/EchoBridge.agda+` previously carried a +"`hand-verified, not machine-checked`" caveat; it now typechecks against +the real `+Echo+` (the `+@+` sensor witness IS +`+Echo (fired sensor thr) true+`). The wider echo-types ↔ typesystem +integration is recorded in echo-types’ +`+docs/bridges/cross-repo-bridge-status.md+`. + +==== Fixed + +* `+kitchenspeak/proofs/agda/PoachedEgg.agda+`: stdlib v2.3 API drift +(`+toWitness {Q = …}+` → `+{a? = …}+`) so the KitchenSpeak proof suite +(Dough + PoachedEgg + EchoBridge) type-checks on the echo-types CI +toolchain (Agda 2.6.3 + stdlib v2.3). + +=== 2026-06-02 + +==== Added + +* KitchenSpeak elevated to standalone-repo-ready and listed as a DSL in +`+README.adoc+` / `+EXPLAINME.adoc+`; +`+scripts/elevate-kitchenspeak.sh+` performs the repo split + submodule +conversion. +* KitchenSpeak proofs commenced: `+PoachedEgg.agda+` +(Linear+Tropical+Echo), `+EchoBridge.agda+`, and a proof harness +(`+proofs/Makefile+`, `+kitchenspeak.agda-lib+`). +* KitchenSpeak ADRs 0002–0004: standalone elevation; `+echo-types+` +dependency; Echo attaches to Linear/Dyadic (B-now / C-later / A-shim). +* Hypatia accepted-findings registry in +`+.machine_readable/6a2/NEUROSYM.a2ml+` `+[waivers]+`, with gitbot +runbook in `+PLAYBOOK.a2ml+` and agent contract in `+AGENTIC.a2ml+`. +* `+6a2+` machine-readable state refreshed +(STATE/META/ECOSYSTEM/NEUROSYM/ PLAYBOOK/AGENTIC); `+MUST.contractile+` +project-specific invariants. + +==== Changed + +* CI hygiene: `+timeout-minutes+` on all real jobs; CodeQL matrix +`+javascript-typescript+` → `+actions+`; scorecard publish job split +from an unprivileged score-gate; `+instant-sync+` dispatch gated on +secret presence; fixed pre-existing invalid YAML in +`+instant-sync.yml+`. +* `+Trustfile+` reconciled: deleting merged PR branches is permitted +(force-push, CI-secret modification, and publish remain denied). + +==== Removed + +* Spurious `+nuget+` ecosystem from `+.github/dependabot.yml+` (no .NET +projects). +* Stale merged feature branches. + +=== 2026-03-15 + +==== Changed + +* Moved 6 design documents to `+docs/design/+` and `+docs/+` for cleaner +root. +* Deleted 14 stale status snapshots, executed plans, and duplicate +files. +* Renamed `+AI.a2ml+` to `+0-AI-MANIFEST.a2ml+` (RSR standard). +* Deleted `+CONTRIBUTING.adoc+` (content subset of `+CONTRIBUTING.md+`). + +==== Removed + +* `+COMPLETION-STATUS-2026-02-07.md+` (stale snapshot) +* `+CONSOLIDATION-COMPLETE.md+` (executed plan) +* `+CONSOLIDATION-PLAN.md+` (executed plan) +* `+FINAL-STATUS-2026-02-07.md+` (stale snapshot) +* `+LANGUAGE-STATUS-MASTER.md+` (superseded) +* `+LANGUAGE-STATUS-VERIFIED-2026-02-07.md+` (stale snapshot) +* `+OBLIBENY-COMPLETION-2026-02-07.md+` (stale snapshot) +* `+MY-LANG-VERIFICATION-BLOCKED.md+` (resolved issue) +* `+MIGRATION-STATUS.md+` (stale, from 2025-12) +* `+MIGRATION-STRATEGY.md+` (executed plan) +* `+MANIFEST.md+` (superseded by 0-AI-MANIFEST.a2ml) +* `+PALIMPSEST.adoc+` (redundant with LICENSE) +* `+CLAUDE-INSTRUCTIONS.md+` (superseded by .claude/CLAUDE.md) +* `+CONTRIBUTING.adoc+` (subset of CONTRIBUTING.md) + +=== 2026-02-07 + +==== Added + +* Consolidation of scattered language repos into canonical locations. +* Updated .machine_readable/6a2/STATE.a2ml with verified completion +percentages. diff --git a/CHANGELOG.md b/CHANGELOG.md deleted file mode 100644 index f0014a2..0000000 --- a/CHANGELOG.md +++ /dev/null @@ -1,91 +0,0 @@ - -# Changelog - -All notable changes to the nextgen-languages parent repository. - -## 2026-06-12 - -### Changed - -- *KitchenSpeak Echo bridge is now MACHINE-CHECKED against the real - `hyperpolymath/echo-types` library.* `kitchenspeak/proofs/agda/EchoBridge.agda` - previously carried a "hand-verified, not machine-checked" caveat; it now - typechecks against the real `Echo` (the `@` sensor witness IS - `Echo (fired sensor thr) true`). The wider echo-types ↔ typesystem - integration is recorded in echo-types' - `docs/bridges/cross-repo-bridge-status.md`. - -### Fixed - -- `kitchenspeak/proofs/agda/PoachedEgg.agda`: stdlib v2.3 API drift - (`toWitness {Q = …}` → `{a? = …}`) so the KitchenSpeak proof suite - (Dough + PoachedEgg + EchoBridge) type-checks on the echo-types CI - toolchain (Agda 2.6.3 + stdlib v2.3). - -## 2026-06-02 - -### Added - -- KitchenSpeak elevated to standalone-repo-ready and listed as a DSL in - `README.adoc` / `EXPLAINME.adoc`; `scripts/elevate-kitchenspeak.sh` performs - the repo split + submodule conversion. -- KitchenSpeak proofs commenced: `PoachedEgg.agda` (Linear+Tropical+Echo), - `EchoBridge.agda`, and a proof harness (`proofs/Makefile`, - `kitchenspeak.agda-lib`). -- KitchenSpeak ADRs 0002–0004: standalone elevation; `echo-types` dependency; - Echo attaches to Linear/Dyadic (B-now / C-later / A-shim). -- Hypatia accepted-findings registry in `.machine_readable/6a2/NEUROSYM.a2ml` - `[waivers]`, with gitbot runbook in `PLAYBOOK.a2ml` and agent contract in - `AGENTIC.a2ml`. -- `6a2` machine-readable state refreshed (STATE/META/ECOSYSTEM/NEUROSYM/ - PLAYBOOK/AGENTIC); `MUST.contractile` project-specific invariants. - -### Changed - -- CI hygiene: `timeout-minutes` on all real jobs; CodeQL matrix - `javascript-typescript` → `actions`; scorecard publish job split from an - unprivileged score-gate; `instant-sync` dispatch gated on secret presence; - fixed pre-existing invalid YAML in `instant-sync.yml`. -- `Trustfile` reconciled: deleting merged PR branches is permitted - (force-push, CI-secret modification, and publish remain denied). - -### Removed - -- Spurious `nuget` ecosystem from `.github/dependabot.yml` (no .NET projects). -- Stale merged feature branches. - -## 2026-03-15 - -### Changed - -- Moved 6 design documents to `docs/design/` and `docs/` for cleaner root. -- Deleted 14 stale status snapshots, executed plans, and duplicate files. -- Renamed `AI.a2ml` to `0-AI-MANIFEST.a2ml` (RSR standard). -- Deleted `CONTRIBUTING.adoc` (content subset of `CONTRIBUTING.md`). - -### Removed - -- `COMPLETION-STATUS-2026-02-07.md` (stale snapshot) -- `CONSOLIDATION-COMPLETE.md` (executed plan) -- `CONSOLIDATION-PLAN.md` (executed plan) -- `FINAL-STATUS-2026-02-07.md` (stale snapshot) -- `LANGUAGE-STATUS-MASTER.md` (superseded) -- `LANGUAGE-STATUS-VERIFIED-2026-02-07.md` (stale snapshot) -- `OBLIBENY-COMPLETION-2026-02-07.md` (stale snapshot) -- `MY-LANG-VERIFICATION-BLOCKED.md` (resolved issue) -- `MIGRATION-STATUS.md` (stale, from 2025-12) -- `MIGRATION-STRATEGY.md` (executed plan) -- `MANIFEST.md` (superseded by 0-AI-MANIFEST.a2ml) -- `PALIMPSEST.adoc` (redundant with LICENSE) -- `CLAUDE-INSTRUCTIONS.md` (superseded by .claude/CLAUDE.md) -- `CONTRIBUTING.adoc` (subset of CONTRIBUTING.md) - -## 2026-02-07 - -### Added - -- Consolidation of scattered language repos into canonical locations. -- Updated .machine_readable/6a2/STATE.a2ml with verified completion percentages. diff --git a/CODE_OF_CONDUCT.adoc b/CODE_OF_CONDUCT.adoc new file mode 100644 index 0000000..bd2a83c --- /dev/null +++ b/CODE_OF_CONDUCT.adoc @@ -0,0 +1,24 @@ +== Contributor Covenant Code of Conduct + +=== Our Pledge + +We pledge to make participation a harassment-free experience for +everyone. + +=== Our Standards + +*Positive behavior:* * Using welcoming language * Being respectful of +differing viewpoints * Accepting constructive criticism * Focusing on +what is best for the community + +*Unacceptable behavior:* * Harassment, trolling, or personal attacks * +Publishing private information without permission + +=== Enforcement + +Report issues to the maintainers. All complaints will be reviewed. + +=== Attribution + +Adapted from https://www.contributor-covenant.org/[Contributor Covenant] +v2.1. diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md deleted file mode 100644 index bbe9219..0000000 --- a/CODE_OF_CONDUCT.md +++ /dev/null @@ -1,30 +0,0 @@ - -# Contributor Covenant Code of Conduct - -## Our Pledge - -We pledge to make participation a harassment-free experience for everyone. - -## Our Standards - -**Positive behavior:** -* Using welcoming language -* Being respectful of differing viewpoints -* Accepting constructive criticism -* Focusing on what is best for the community - -**Unacceptable behavior:** -* Harassment, trolling, or personal attacks -* Publishing private information without permission - -## Enforcement - -Report issues to the maintainers. All complaints will be reviewed. - -## Attribution - -Adapted from [Contributor Covenant](https://www.contributor-covenant.org/) v2.1. - diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc new file mode 100644 index 0000000..5017c98 --- /dev/null +++ b/CONTRIBUTING.adoc @@ -0,0 +1,109 @@ +== Clone the repository + +git clone https://github.com/hyperpolymath/nextgen-languages.git cd +nextgen-languages + +== Using Nix (recommended for reproducibility) + +nix develop + +== Or using toolbox/distrobox + +toolbox create nextgen-languages-dev toolbox enter nextgen-languages-dev +# Install dependencies manually + +== Verify setup + +just check # or: cargo check / mix compile / etc. just test # Run test +suite + +.... + +### Repository Structure +.... + +nextgen-languages/ ├── src/ # Source code (Perimeter 1-2) ├── lib/ # +Library code (Perimeter 1-2) ├── extensions/ # Extensions (Perimeter 2) +├── plugins/ # Plugins (Perimeter 2) ├── tools/ # Tooling (Perimeter 2) +├── docs/ # Documentation (Perimeter 3) │ ├── architecture/ # ADRs, +specs (Perimeter 2) │ └── proposals/ # RFCs (Perimeter 3) ├── examples/ +# Examples (Perimeter 3) ├── spec/ # Spec tests (Perimeter 3) ├── tests/ +# Test suite (Perimeter 2-3) ├── .well-known/ # Protocol files +(Perimeter 1-3) ├── .github/ # GitHub config (Perimeter 1) │ ├── +ISSUE_TEMPLATE/ │ └── workflows/ ├── CHANGELOG.md ├── CODE_OF_CONDUCT.md +├── CONTRIBUTING.md # This file ├── GOVERNANCE.md ├── LICENSE ├── +MAINTAINERS.md ├── README.adoc ├── SECURITY.md └── Justfile # Task +runner (Perimeter 1) + +.... + +--- + +## How to Contribute + +### Reporting Bugs + +**Before reporting**: +1. Search existing issues +2. Check if it's already fixed in `main` +3. Determine which perimeter the bug affects + +**When reporting**: + +Use the [bug report template](.github/ISSUE_TEMPLATE/bug_report.md) and include: + +- Clear, descriptive title +- Environment details (OS, versions, toolchain) +- Steps to reproduce +- Expected vs actual behaviour +- Logs, screenshots, or minimal reproduction + +### Suggesting Features + +**Before suggesting**: +1. Check the [roadmap](ROADMAP.md) if available +2. Search existing issues and discussions +3. Consider which perimeter the feature belongs to + +**When suggesting**: + +Use the [feature request template](.github/ISSUE_TEMPLATE/feature_request.md) and include: + +- Problem statement (what pain point does this solve?) +- Proposed solution +- Alternatives considered +- Which perimeter this affects + +### Your First Contribution + +Look for issues labelled: + +- [`good first issue`](https://github.com/hyperpolymath/nextgen-languages/labels/good%20first%20issue) — Simple Perimeter 3 tasks +- [`help wanted`](https://github.com/hyperpolymath/nextgen-languages/labels/help%20wanted) — Community help needed +- [`documentation`](https://github.com/hyperpolymath/nextgen-languages/labels/documentation) — Docs improvements +- [`perimeter-3`](https://github.com/hyperpolymath/nextgen-languages/labels/perimeter-3) — Community sandbox scope + +--- + +## Development Workflow + +### Branch Naming +.... + +docs/short-description # Documentation (P3) test/what-added # Test +additions (P3) feat/short-description # New features (P2) +fix/issue-number-description # Bug fixes (P2) refactor/what-changed # +Code improvements (P2) security/what-fixed # Security fixes (P1-2) + +.... + +### Commit Messages + +We follow [Conventional Commits](https://www.conventionalcommits.org/): +.... + +(): + +{empty}[optional body] + +{empty}[optional footer] diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md deleted file mode 100644 index 6c2387a..0000000 --- a/CONTRIBUTING.md +++ /dev/null @@ -1,119 +0,0 @@ - -# Clone the repository -git clone https://github.com/hyperpolymath/nextgen-languages.git -cd nextgen-languages - -# Using Nix (recommended for reproducibility) -nix develop - -# Or using toolbox/distrobox -toolbox create nextgen-languages-dev -toolbox enter nextgen-languages-dev -# Install dependencies manually - -# Verify setup -just check # or: cargo check / mix compile / etc. -just test # Run test suite -``` - -### Repository Structure -``` -nextgen-languages/ -├── src/ # Source code (Perimeter 1-2) -├── lib/ # Library code (Perimeter 1-2) -├── extensions/ # Extensions (Perimeter 2) -├── plugins/ # Plugins (Perimeter 2) -├── tools/ # Tooling (Perimeter 2) -├── docs/ # Documentation (Perimeter 3) -│ ├── architecture/ # ADRs, specs (Perimeter 2) -│ └── proposals/ # RFCs (Perimeter 3) -├── examples/ # Examples (Perimeter 3) -├── spec/ # Spec tests (Perimeter 3) -├── tests/ # Test suite (Perimeter 2-3) -├── .well-known/ # Protocol files (Perimeter 1-3) -├── .github/ # GitHub config (Perimeter 1) -│ ├── ISSUE_TEMPLATE/ -│ └── workflows/ -├── CHANGELOG.md -├── CODE_OF_CONDUCT.md -├── CONTRIBUTING.md # This file -├── GOVERNANCE.md -├── LICENSE -├── MAINTAINERS.md -├── README.adoc -├── SECURITY.md -└── Justfile # Task runner (Perimeter 1) -``` - ---- - -## How to Contribute - -### Reporting Bugs - -**Before reporting**: -1. Search existing issues -2. Check if it's already fixed in `main` -3. Determine which perimeter the bug affects - -**When reporting**: - -Use the [bug report template](.github/ISSUE_TEMPLATE/bug_report.md) and include: - -- Clear, descriptive title -- Environment details (OS, versions, toolchain) -- Steps to reproduce -- Expected vs actual behaviour -- Logs, screenshots, or minimal reproduction - -### Suggesting Features - -**Before suggesting**: -1. Check the [roadmap](ROADMAP.md) if available -2. Search existing issues and discussions -3. Consider which perimeter the feature belongs to - -**When suggesting**: - -Use the [feature request template](.github/ISSUE_TEMPLATE/feature_request.md) and include: - -- Problem statement (what pain point does this solve?) -- Proposed solution -- Alternatives considered -- Which perimeter this affects - -### Your First Contribution - -Look for issues labelled: - -- [`good first issue`](https://github.com/hyperpolymath/nextgen-languages/labels/good%20first%20issue) — Simple Perimeter 3 tasks -- [`help wanted`](https://github.com/hyperpolymath/nextgen-languages/labels/help%20wanted) — Community help needed -- [`documentation`](https://github.com/hyperpolymath/nextgen-languages/labels/documentation) — Docs improvements -- [`perimeter-3`](https://github.com/hyperpolymath/nextgen-languages/labels/perimeter-3) — Community sandbox scope - ---- - -## Development Workflow - -### Branch Naming -``` -docs/short-description # Documentation (P3) -test/what-added # Test additions (P3) -feat/short-description # New features (P2) -fix/issue-number-description # Bug fixes (P2) -refactor/what-changed # Code improvements (P2) -security/what-fixed # Security fixes (P1-2) -``` - -### Commit Messages - -We follow [Conventional Commits](https://www.conventionalcommits.org/): -``` -(): - -[optional body] - -[optional footer] diff --git a/EXTRACTION-MANIFEST.adoc b/EXTRACTION-MANIFEST.adoc new file mode 100644 index 0000000..be4f1a0 --- /dev/null +++ b/EXTRACTION-MANIFEST.adoc @@ -0,0 +1,157 @@ +== Extraction Manifest + +`+nextgen-languages+` is a *pure coordinator*. This file records +language-specific content that had leaked into the coordinator and where +it belongs, so it can be landed in each language’s own +`+hyperpolymath/+` repo and then removed from here. + +*Why a manifest instead of a direct move:* the session that produced +this change had GitHub access scoped to +`+hyperpolymath/nextgen-languages+` only — it could not push into the +sibling repos. So content that is *not already superseded upstream* was +_staged_ under `+extraction-queue/+` (excluded from the +coordinator-boundary guard) rather than deleted, to avoid data loss. Git +history preserves everything regardless. + +=== How to land a staged item (for a maintainer / cross-repo session) + +[source,sh] +---- +# Example: AffineScript's wiki page → the affinescript repo +# (in a checkout/session that has hyperpolymath/affinescript in scope) +git mv extraction-queue/affinescript/wiki-AffineScript.md \ + /wiki/AffineScript.md # or docs/, per that repo's convention +# ...repeat for each row below, then: +git rm -r extraction-queue// # once that language's items have landed +---- + +When `+extraction-queue/+` is empty, delete it. The +`+coordinator-boundary+` CI check keeps new language content from +reappearing. + +''''' + +=== A. Deleted here (already superseded upstream — no action needed) + +[width="100%",cols="34%,33%,33%",options="header",] +|=== +|Removed path |Canonical home |Why safe to delete +|`+kitchenspeak/**+` (entire subtree: SPEC, grammar.ebnf, +proofs/agda/_.agda, examples/_.ks, decisions/*, ROADMAP, CHANGELOG, +COMMENTARY, MOVED.adoc) |`+hyperpolymath/kitchenspeak+` |Was a frozen +v1.0 snapshot; the standalone repo carries a superseding v2.0 +(physics-in-types, OCaml compiler, machine-checked Agda). Its own +`+MOVED.adoc+` pre-authorized removal. + +|`+scripts/elevate-kitchenspeak.sh+` |n/a |One-shot elevation tool; +elevation is complete. + +|`+languages/kitchenspeak.md+` |`+hyperpolymath/kitchenspeak+` |Orphan +coordinator stub (not in the `+languages/+` index); content superseded +upstream. +|=== + +=== B. Staged in `+extraction-queue/+` — pending landing in the sibling repo + +Each was moved out of the coordinator’s active surface +(`+wiki/languages/+`, `+docs/design/+`, or the README) into +`+extraction-queue//+`. *These are NOT yet in their destination +repos* — land them, then delete the staged copy. + +[width="100%",cols="25%,25%,25%,25%",options="header",] +|=== +|Staged path |Destination repo |Suggested target |Notes +|`+extraction-queue/affinescript/wiki-AffineScript.md+` +|`+hyperpolymath/affinescript+` |`+wiki/AffineScript.md+` |from +`+wiki/languages/+` + +|`+extraction-queue/ephapax/wiki-Ephapax.md+` |`+hyperpolymath/ephapax+` +|`+wiki/Ephapax.md+` |from `+wiki/languages/+` + +|`+extraction-queue/ephapax/design/dyadic-architecture.md+` +|`+hyperpolymath/ephapax+` |`+docs/design/dyadic-architecture.md+` |from +`+docs/design/+` + +|`+extraction-queue/ephapax/design/proven-integration.md+` +|`+hyperpolymath/ephapax+` |`+docs/design/proven-integration.md+` |from +`+docs/design/+` + +|`+extraction-queue/anvomidav/wiki-Anvomidav.md+` +|`+hyperpolymath/anvomidav+` |`+wiki/Anvomidav.md+` |from +`+wiki/languages/+` + +|`+extraction-queue/eclexia/wiki-Eclexia.md+` |`+hyperpolymath/eclexia+` +|`+wiki/Eclexia.md+` |from `+wiki/languages/+` + +|`+extraction-queue/eclexia/design/next-steps.md+` +|`+hyperpolymath/eclexia+` |`+docs/design/next-steps.md+` |from +`+docs/design/+` + +|`+extraction-queue/betlang/wiki-betlang.md+` |`+hyperpolymath/betlang+` +|`+wiki/betlang.md+` |from `+wiki/languages/+` + +|`+extraction-queue/jtv/wiki-jtv.md+` |`+hyperpolymath/jtv+` +|`+wiki/jtv.md+` |from `+wiki/languages/+` + +|`+extraction-queue/jtv/design/007-reversibility-fork.adoc+` +|`+hyperpolymath/jtv+` |`+docs/design/007-reversibility-fork.adoc+` +|from `+docs/design/+` + +|`+extraction-queue/oblibeny/wiki-Oblibeny.md+` +|`+hyperpolymath/oblibeny+` |`+wiki/Oblibeny.md+` |from +`+wiki/languages/+` + +|`+extraction-queue/phronesis/wiki-Phronesis.md+` +|`+hyperpolymath/phronesis+` |`+wiki/Phronesis.md+` |from +`+wiki/languages/+` + +|`+extraction-queue/wokelang/wiki-WokeLang.md+` +|`+hyperpolymath/wokelang+` |`+wiki/WokeLang.md+` |from +`+wiki/languages/+` + +|`+extraction-queue/my-lang/wiki-My-Language-Family.md+` +|`+hyperpolymath/my-lang+` |`+wiki/My-Language-Family.md+` |from +`+wiki/languages/+` + +|`+extraction-queue/my-lang/wiki-Solo.md+` |`+hyperpolymath/my-lang+` +|`+wiki/Solo.md+` |dialect + +|`+extraction-queue/my-lang/wiki-Duet.md+` |`+hyperpolymath/my-lang+` +|`+wiki/Duet.md+` |dialect + +|`+extraction-queue/my-lang/wiki-Ensemble.md+` +|`+hyperpolymath/my-lang+` |`+wiki/Ensemble.md+` |dialect + +|`+extraction-queue/my-lang/wiki-Me.md+` |`+hyperpolymath/my-lang+` +|`+wiki/Me.md+` |*FIX on landing:* this page models "`Me`" as a fourth +dialect. Me is an _agent-generated projection_ over Solo/Duet/Ensemble +(see `+tentacles-agentic-syllabus/me/README.adoc+`), not a static +dialect. + +|`+extraction-queue/typefix-zero/SPEC.adoc+` |`+typefix-zero+` _(private +repo; viability under review; not in ECOSYSTEM.a2ml)_ |`+SPEC.adoc+` +|Was a headingless spec dump pasted into `+README.adoc+`. Land in the +private repo if/when its viability is confirmed. +|=== + +=== C. Kept in the coordinator (cross-language — correctly belongs here) + +[width="100%",cols="50%,50%",options="header",] +|=== +|Path |Why it stays +|`+docs/disambiguation/ephapax-vs-affinescript.md+` |Cross-language +anti-confusion doc; its whole purpose is to span two repos. + +|`+wiki/overview/+`, `+wiki/tooling/+`, `+wiki/tutorials/+`, +`+wiki/frameworks/+` |Language-_agnostic_ education. Candidate for later +relocation to `+hyperpolymath/tentacles-agentic-syllabus+` (curriculum), +but not language-specific leakage. + +|`+docs/design/verisim-parallel-dev.adoc+` |Cross-cutting +language↔VeriSim co-development note. Could later move to +`+hyperpolymath/verisimdb+`. + +|`+TEST-NEEDS.md+`, `+PROOF-NEEDS.md+`, `+TOOLING-STATUS.adoc+`, +`+language-status-tracker.jl+` |Cross-language trackers — the +coordinator’s core job. +|=== diff --git a/EXTRACTION-MANIFEST.md b/EXTRACTION-MANIFEST.md deleted file mode 100644 index 1407400..0000000 --- a/EXTRACTION-MANIFEST.md +++ /dev/null @@ -1,76 +0,0 @@ - -# Extraction Manifest - -`nextgen-languages` is a **pure coordinator**. This file records language-specific content -that had leaked into the coordinator and where it belongs, so it can be landed in each -language's own `hyperpolymath/` repo and then removed from here. - -**Why a manifest instead of a direct move:** the session that produced this change had GitHub -access scoped to `hyperpolymath/nextgen-languages` only — it could not push into the sibling -repos. So content that is **not already superseded upstream** was *staged* under -`extraction-queue/` (excluded from the coordinator-boundary guard) rather than deleted, to -avoid data loss. Git history preserves everything regardless. - -## How to land a staged item (for a maintainer / cross-repo session) - -```sh -# Example: AffineScript's wiki page → the affinescript repo -# (in a checkout/session that has hyperpolymath/affinescript in scope) -git mv extraction-queue/affinescript/wiki-AffineScript.md \ - /wiki/AffineScript.md # or docs/, per that repo's convention -# ...repeat for each row below, then: -git rm -r extraction-queue// # once that language's items have landed -``` - -When `extraction-queue/` is empty, delete it. The `coordinator-boundary` CI check keeps new -language content from reappearing. - ---- - -## A. Deleted here (already superseded upstream — no action needed) - -| Removed path | Canonical home | Why safe to delete | -|---|---|---| -| `kitchenspeak/**` (entire subtree: SPEC, grammar.ebnf, proofs/agda/*.agda, examples/*.ks, decisions/*, ROADMAP, CHANGELOG, COMMENTARY, MOVED.adoc) | `hyperpolymath/kitchenspeak` | Was a frozen v1.0 snapshot; the standalone repo carries a superseding v2.0 (physics-in-types, OCaml compiler, machine-checked Agda). Its own `MOVED.adoc` pre-authorized removal. | -| `scripts/elevate-kitchenspeak.sh` | n/a | One-shot elevation tool; elevation is complete. | -| `languages/kitchenspeak.md` | `hyperpolymath/kitchenspeak` | Orphan coordinator stub (not in the `languages/` index); content superseded upstream. | - -## B. Staged in `extraction-queue/` — pending landing in the sibling repo - -Each was moved out of the coordinator's active surface (`wiki/languages/`, `docs/design/`, -or the README) into `extraction-queue//`. **These are NOT yet in their destination -repos** — land them, then delete the staged copy. - -| Staged path | Destination repo | Suggested target | Notes | -|---|---|---|---| -| `extraction-queue/affinescript/wiki-AffineScript.md` | `hyperpolymath/affinescript` | `wiki/AffineScript.md` | from `wiki/languages/` | -| `extraction-queue/ephapax/wiki-Ephapax.md` | `hyperpolymath/ephapax` | `wiki/Ephapax.md` | from `wiki/languages/` | -| `extraction-queue/ephapax/design/dyadic-architecture.md` | `hyperpolymath/ephapax` | `docs/design/dyadic-architecture.md` | from `docs/design/` | -| `extraction-queue/ephapax/design/proven-integration.md` | `hyperpolymath/ephapax` | `docs/design/proven-integration.md` | from `docs/design/` | -| `extraction-queue/anvomidav/wiki-Anvomidav.md` | `hyperpolymath/anvomidav` | `wiki/Anvomidav.md` | from `wiki/languages/` | -| `extraction-queue/eclexia/wiki-Eclexia.md` | `hyperpolymath/eclexia` | `wiki/Eclexia.md` | from `wiki/languages/` | -| `extraction-queue/eclexia/design/next-steps.md` | `hyperpolymath/eclexia` | `docs/design/next-steps.md` | from `docs/design/` | -| `extraction-queue/betlang/wiki-betlang.md` | `hyperpolymath/betlang` | `wiki/betlang.md` | from `wiki/languages/` | -| `extraction-queue/jtv/wiki-jtv.md` | `hyperpolymath/jtv` | `wiki/jtv.md` | from `wiki/languages/` | -| `extraction-queue/jtv/design/007-reversibility-fork.adoc` | `hyperpolymath/jtv` | `docs/design/007-reversibility-fork.adoc` | from `docs/design/` | -| `extraction-queue/oblibeny/wiki-Oblibeny.md` | `hyperpolymath/oblibeny` | `wiki/Oblibeny.md` | from `wiki/languages/` | -| `extraction-queue/phronesis/wiki-Phronesis.md` | `hyperpolymath/phronesis` | `wiki/Phronesis.md` | from `wiki/languages/` | -| `extraction-queue/wokelang/wiki-WokeLang.md` | `hyperpolymath/wokelang` | `wiki/WokeLang.md` | from `wiki/languages/` | -| `extraction-queue/my-lang/wiki-My-Language-Family.md` | `hyperpolymath/my-lang` | `wiki/My-Language-Family.md` | from `wiki/languages/` | -| `extraction-queue/my-lang/wiki-Solo.md` | `hyperpolymath/my-lang` | `wiki/Solo.md` | dialect | -| `extraction-queue/my-lang/wiki-Duet.md` | `hyperpolymath/my-lang` | `wiki/Duet.md` | dialect | -| `extraction-queue/my-lang/wiki-Ensemble.md` | `hyperpolymath/my-lang` | `wiki/Ensemble.md` | dialect | -| `extraction-queue/my-lang/wiki-Me.md` | `hyperpolymath/my-lang` | `wiki/Me.md` | **FIX on landing:** this page models "Me" as a fourth dialect. Me is an *agent-generated projection* over Solo/Duet/Ensemble (see `tentacles-agentic-syllabus/me/README.adoc`), not a static dialect. | -| `extraction-queue/typefix-zero/SPEC.adoc` | `typefix-zero` *(private repo; viability under review; not in ECOSYSTEM.a2ml)* | `SPEC.adoc` | Was a headingless spec dump pasted into `README.adoc`. Land in the private repo if/when its viability is confirmed. | - -## C. Kept in the coordinator (cross-language — correctly belongs here) - -| Path | Why it stays | -|---|---| -| `docs/disambiguation/ephapax-vs-affinescript.md` | Cross-language anti-confusion doc; its whole purpose is to span two repos. | -| `wiki/overview/`, `wiki/tooling/`, `wiki/tutorials/`, `wiki/frameworks/` | Language-*agnostic* education. Candidate for later relocation to `hyperpolymath/tentacles-agentic-syllabus` (curriculum), but not language-specific leakage. | -| `docs/design/verisim-parallel-dev.adoc` | Cross-cutting language↔VeriSim co-development note. Could later move to `hyperpolymath/verisimdb`. | -| `TEST-NEEDS.md`, `PROOF-NEEDS.md`, `TOOLING-STATUS.adoc`, `language-status-tracker.jl` | Cross-language trackers — the coordinator's core job. | diff --git a/GOVERNANCE.adoc b/GOVERNANCE.adoc index e41020d..9b836fb 100644 --- a/GOVERNANCE.adoc +++ b/GOVERNANCE.adoc @@ -1,162 +1,60 @@ -// SPDX-License-Identifier: CC-BY-SA-4.0 -// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -= Governance Model -:toc: preamble +== Governance -This document describes the governance model for this repository. +=== Overview -== Overview +This project is governed by the following principles and structures to +ensure transparent, inclusive, and effective decision-making. -This repository follows a **Sole Maintainer Governance Model**: +=== Roles and Responsibilities -* Single maintainer (@hyperpolymath) has full authority over the project -* All contributions are welcome and reviewed by the maintainer -* Decisions are made transparently through GitHub issues and discussions -* The project adheres to the hyperpolymath estate policies where applicable +==== Maintainers -== Core Principles +Maintainers are responsible for: - Reviewing and merging pull requests - +Managing releases and versioning - Ensuring code quality and standards - +Triaging issues and bug reports - Community engagement and support -[cols="1,2"] -|=== -| Principle | Description +==== Contributors -| **Benevolent Dictatorship** | Maintainer has final decision authority but seeks community input +Contributors are expected to: - Follow the code of conduct - Submit +well-documented pull requests - Write tests for new functionality - +Maintain existing tests - Update documentation as needed -| **Meritocracy** | Contributions are judged on technical merit, not contributor identity +=== Decision Making -| **Transparency** | All significant decisions are documented publicly +==== Minor Changes -| **Consensus-Seeking** | Maintainer prefers consensus but will decide when necessary +* Can be made by any maintainer +* Include bug fixes, documentation updates, dependency updates -| **Open Contribution** | Anyone can contribute via fork and pull request +==== Major Changes -|=== +* Require discussion in issues or pull requests +* Include new features, architectural changes, API changes +* Need approval from at least 2 maintainers -== Roles and Permissions +==== Breaking Changes -[cols="1,2,2"] -|=== -| Role | Permissions | Assignment +* Require RFC (Request for Comments) process +* Need approval from majority of maintainers +* Must include migration guide -| **Maintainer** | Write access, merge rights, admin | @hyperpolymath -| **Contributors** | Read access, fork, submit PRs | All GitHub users -| **Users** | Use the software, report issues | All GitHub users +=== Code of Conduct -|=== +All participants are expected to follow our Code of Conduct. Violations +can be reported to the maintainers. -== Decision Making Framework +=== Communication -=== Routine Decisions +* *Issues*: For bug reports and feature requests +* *Discussions*: For questions and general discussion +* *Pull Requests*: For code contributions -* Bug fixes -* Documentation improvements -* Minor feature additions -* Dependency updates +=== Licensing -**Process**: Maintainer reviews and merges PRs that meet quality standards. +All contributions are made under the terms of the repository’s LICENSE +file. By submitting a pull request, you agree to license your +contributions accordingly. -=== Significant Changes +''''' -* New major features -* API changes -* Architecture modifications -* Breaking changes - -**Process**: -. Open issue describing the change -. Discuss with community (minimum 72 hours) -. Maintainer makes final decision -. Document rationale in issue/PR - -=== Structural Decisions - -* Repository purpose/renaming -* License changes -* Ownership transfer -* Deprecation/archival - -**Process**: -. Extended discussion (minimum 1 week) -. Maintainer makes final decision -. Document in CHANGELOG and governance docs - -== Contribution Lifecycle - -[cols="1,2"] -|=== -| Stage | Process - -| **Ideation** | Open issue, discuss feasibility - -| **Development** | Fork, implement, test thoroughly - -| **Review** | Submit PR, maintainer reviews within 7 days - -| **Merge** | Maintainer merges or requests changes - -| **Release** | Maintainer publishes according to project conventions - -|=== - -== Conflict Resolution - -In case of disagreements: - -. Discuss in the relevant GitHub issue or PR -. Provide technical justification for positions -. Maintainer mediates and makes final decision -. Decision is documented and can be revisited later - -== Project Policies - -This repository adheres to hyperpolymath estate-wide policies: - -* **License**: MPL-2.0 for code, CC-BY-SA-4.0 for prose (per standards/LICENCE-POLICY.adoc) -* **Code of Conduct**: Follows hyperpolymath CODE_OF_CONDUCT.md -* **Security**: Follows hyperpolymath SECURITY.md -* **Contributing**: Follows hyperpolymath CONTRIBUTING.adoc conventions - -== Repository-Specific Conventions - -[cols="1,2"] -|=== -| Convention | Description - -| **Signing** | All commits must be signed (SSH or GPG) - -| **SPDX Headers** | All source files must have SPDX license identifiers - -| **Contractiles** | Mustfile, Trustfile, Intendfile, Adjustfile in root - -| **Machine Readable** | META.a2ml in .machine_readable/6a2/ - -| **CI/CD** | GitHub Actions workflows in .github/workflows/ - -|=== - -== Governance Evolution - -As the project grows, this governance model may evolve: - -* **Adding Co-Maintainers**: When contribution volume warrants it -* **Forming a Team**: For complex multi-maintainer projects -* **Adopting TPCF**: For large, multi-repository projects (see rhodium-standard-repositories) - -Changes to this document require the same process as Significant Changes above. - -== See Also - -* link:MAINTAINERS.adoc[Maintainers] -* link:CODE_OF_CONDUCT.md[Code of Conduct] -* link:CONTRIBUTING.adoc[Contributing Guide] -* link:https://github.com/hyperpolymath/standards/blob/main/LICENCE-POLICY.adoc[Estate License Policy] -* link:https://github.com/hyperpolymath/standards[rhodium-standard-repositories (TPCF)] - -== Changelog - -[cols="1,1,1"] -|=== -| Date | Change | By - -| 2026-06-07 | Initial governance model established | @hyperpolymath -|=== +_Last updated: 2026-07-18_ diff --git a/GOVERNANCE.md b/GOVERNANCE.md deleted file mode 100644 index e27364c..0000000 --- a/GOVERNANCE.md +++ /dev/null @@ -1,60 +0,0 @@ -# Governance - -## Overview - -This project is governed by the following principles and structures to ensure transparent, inclusive, and effective decision-making. - -## Roles and Responsibilities - -### Maintainers - -Maintainers are responsible for: -- Reviewing and merging pull requests -- Managing releases and versioning -- Ensuring code quality and standards -- Triaging issues and bug reports -- Community engagement and support - -### Contributors - -Contributors are expected to: -- Follow the code of conduct -- Submit well-documented pull requests -- Write tests for new functionality -- Maintain existing tests -- Update documentation as needed - -## Decision Making - -### Minor Changes -- Can be made by any maintainer -- Include bug fixes, documentation updates, dependency updates - -### Major Changes -- Require discussion in issues or pull requests -- Include new features, architectural changes, API changes -- Need approval from at least 2 maintainers - -### Breaking Changes -- Require RFC (Request for Comments) process -- Need approval from majority of maintainers -- Must include migration guide - -## Code of Conduct - -All participants are expected to follow our Code of Conduct. Violations can be reported to the maintainers. - -## Communication - -- **Issues**: For bug reports and feature requests -- **Discussions**: For questions and general discussion -- **Pull Requests**: For code contributions - -## Licensing - -All contributions are made under the terms of the repository's LICENSE file. -By submitting a pull request, you agree to license your contributions accordingly. - ---- - -*Last updated: 2026-07-18* diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc new file mode 100644 index 0000000..488c164 --- /dev/null +++ b/PROOF-NEEDS.adoc @@ -0,0 +1,70 @@ +== PROOF-NEEDS.md — nextgen-languages + +=== Current State + +`+nextgen-languages+` is a pure coordinator and holds *no* proof code. +This file tracks the family’s proof gaps across the standalone +`+hyperpolymath/+` repos; every path below is relative to the +named language’s own repo, not this one. + +* *Ephapax* — Coq proofs present; 4 `+Admitted+` remain in +`+formal/Semantics.v+` (ctx_transfer 15/24, subst_lemma, preservation, + +one more). +* *Tangle* — Lean proofs present (`+Tangle.lean+`); coverage partial. +* *Oblíbený* — Idris2 ABI present (`+src/abi/Interface.idr+`); minimal. +* *AffineScript* — OCaml type checker + Rust runtime; soundness proofs +outstanding. + +=== What Needs Proving + +[width="100%",cols="51%,27%,22%",options="header",] +|=== +|Component |What |Why +|Ephapax ctx_transfer (15/24 cases) |Close remaining 9 context transfer +cases in Semantics.v |Core type safety theorem is incomplete + +|Ephapax subst_lemma |Prove substitution lemma |Required for +preservation theorem + +|Ephapax preservation |Close preservation theorem (depends on +subst_lemma) |Type preservation is THE fundamental safety property + +|Ephapax 4th Admitted |Close the 4th Admitted in Semantics.v |Blocks +full formal verification claim + +|AffineScript type safety |Prove OCaml type checker is sound +|AffineScript claims affine types but lacks proofs + +|AffineScript runtime (Rust) |GC and allocator correctness |Memory +safety of the runtime is critical + +|Betlang type checker |Prove bet-check is sound |Compiler correctness +depends on type checking + +|Tangle Lean proofs |Extend Tangle.lean coverage |Existing Lean proofs +are partial + +|Oblibeny ABI |Extend Interface.idr with full package proofs |Current +ABI is minimal +|=== + +=== KitchenSpeak + +KitchenSpeak is now an external standalone repo; its Agda proofs and +their trusted base (postulated echo-oracles / sensors and the GENTLE +controller spec) live in `+hyperpolymath/kitchenspeak+`, not in this +coordinator. + +=== Recommended Prover + +*Coq* for Ephapax (existing proof infrastructure). *Lean4* for Tangle +(existing). *Idris2* for ABI layers. *OCaml* extraction from Coq for +AffineScript type checker verification. + +=== Priority + +*HIGH* — These are programming language compilers. Type safety proofs +are the gold standard for language correctness. The 4 Admitted proofs in +Ephapax are concrete, known gaps that block the formal verification +claim. AffineScript’s runtime Rust code (GC, allocator) is +safety-critical. diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md deleted file mode 100644 index 07f0877..0000000 --- a/PROOF-NEEDS.md +++ /dev/null @@ -1,44 +0,0 @@ - -# PROOF-NEEDS.md — nextgen-languages - -## Current State - -`nextgen-languages` is a pure coordinator and holds **no** proof code. This file tracks the -family's proof gaps across the standalone `hyperpolymath/` repos; every path below is -relative to the named language's own repo, not this one. - -- **Ephapax** — Coq proofs present; 4 `Admitted` remain in `formal/Semantics.v` (ctx_transfer 15/24, subst_lemma, preservation, + one more). -- **Tangle** — Lean proofs present (`Tangle.lean`); coverage partial. -- **Oblíbený** — Idris2 ABI present (`src/abi/Interface.idr`); minimal. -- **AffineScript** — OCaml type checker + Rust runtime; soundness proofs outstanding. - -## What Needs Proving - -| Component | What | Why | -|-----------|------|-----| -| Ephapax ctx_transfer (15/24 cases) | Close remaining 9 context transfer cases in Semantics.v | Core type safety theorem is incomplete | -| Ephapax subst_lemma | Prove substitution lemma | Required for preservation theorem | -| Ephapax preservation | Close preservation theorem (depends on subst_lemma) | Type preservation is THE fundamental safety property | -| Ephapax 4th Admitted | Close the 4th Admitted in Semantics.v | Blocks full formal verification claim | -| AffineScript type safety | Prove OCaml type checker is sound | AffineScript claims affine types but lacks proofs | -| AffineScript runtime (Rust) | GC and allocator correctness | Memory safety of the runtime is critical | -| Betlang type checker | Prove bet-check is sound | Compiler correctness depends on type checking | -| Tangle Lean proofs | Extend Tangle.lean coverage | Existing Lean proofs are partial | -| Oblibeny ABI | Extend Interface.idr with full package proofs | Current ABI is minimal | - -## KitchenSpeak - -KitchenSpeak is now an external standalone repo; its Agda proofs and their -trusted base (postulated echo-oracles / sensors and the GENTLE controller -spec) live in `hyperpolymath/kitchenspeak`, not in this coordinator. - -## Recommended Prover - -**Coq** for Ephapax (existing proof infrastructure). **Lean4** for Tangle (existing). **Idris2** for ABI layers. **OCaml** extraction from Coq for AffineScript type checker verification. - -## Priority - -**HIGH** — These are programming language compilers. Type safety proofs are the gold standard for language correctness. The 4 Admitted proofs in Ephapax are concrete, known gaps that block the formal verification claim. AffineScript's runtime Rust code (GC, allocator) is safety-critical. diff --git a/REQUIRES_INITIALISATION.adoc b/REQUIRES_INITIALISATION.adoc new file mode 100644 index 0000000..a1e481d --- /dev/null +++ b/REQUIRES_INITIALISATION.adoc @@ -0,0 +1,122 @@ +== REQUIRES INITIALISATION + +*This repository is not finished being set up.* 9 substitution token(s) +across 6 file(s) still have no value. + +=== Why this is not already done + +This repo was created from `+hyperpolymath/rsr-template-repo+`. The mint +(`+just repo-init+`) fills every token that has a single mechanical +answer — owner, repo, author, dates, licence, branch — and it has done +so here. + +The tokens below are the ones it _deliberately cannot_ answer. They need +a decision or a fact that exists only in your head: what this project is +for, what command builds it, which port the service listens on, whether +a PGP key is held at all. The template’s own token vocabulary says as +much — you cannot sensibly answer "`required invariants`" in a +thirty-second bootstrap. + +They were left *visibly unfilled on purpose*. The alternatives were both +worse: inventing plausible values would put confident falsehoods into a +security policy and an architecture document, and silently deleting the +sections would hide the fact that a decision is owed. A visible gap is +honest; a fabricated answer is not. + +=== Do not delete this file until every item below is resolved + +This file is the only marker that the work is outstanding. Deleting it +early does not finish the setup, it just conceals it — and the next +person or agent to arrive will reasonably assume the repo is complete. + +* *If you are a person:* delete this file yourself once the last item is +done. +* *If you are an agent:* resolve what you legitimately can, leave the +rest, and delete this file only when no token below remains anywhere in +the tree. Do not delete it to make a gate go green. + +Re-running the estate top-up tool will remove this file automatically +once nothing is outstanding, so the safest way to finish is to fix the +tokens and let the check confirm it. + +=== What is needed, and where it goes + +==== `+{{BUILD_CMD}}+` + +The exact command that builds this project. + +Appears in: + +* `+QUICKSTART-DEV.adoc+` + +==== `+{{BUILD_OUTPUT_PATH}}+` + +Where the build artefact lands. + +Appears in: + +* `+QUICKSTART-MAINTAINER.adoc+` + +==== `+{{DEPS}}+` + +Prose summary of runtime/build dependencies. + +Appears in: + +* `+QUICKSTART-MAINTAINER.adoc+` + +==== `+{{LANG_STACK}}+` + +The language stack, in prose. + +Appears in: + +* `+QUICKSTART-DEV.adoc+` + +==== `+{{MUST_INVARIANTS}}+` + +The invariants this project guarantees. Not answerable in a bootstrap; +it is the point of the repo. + +Appears in: + +* `+QUICKSTART-DEV.adoc+` + +==== `+{{PROJECT_UNIQUE_STRENGTH}}+` + +What this does that its alternatives do not. + +Appears in: + +* `+.machine_readable/bot_directives/methodology.a2ml+` +* `+.machine_readable/svc/k9/methodology-guard.k9.ncl+` + +==== `+{{QUERY}}+` + +Appears in: + +* `+.machine_readable/contractiles/Justfile+` +* `+Justfile+` + +==== `+{{TEST_CMD}}+` + +The exact command that runs its tests. + +Appears in: + +* `+QUICKSTART-DEV.adoc+` + +==== `+{{VERSION}}+` + +Version/tag for the container image. + +Appears in: + +* `+.machine_readable/contractiles/Justfile+` +* `+Justfile+` + +''''' + +Generated by the estate top-up pass. Rationale and the governing rulings +are in `+hyperpolymath/standards+`; the token vocabulary is +`+.machine_readable/ai/PLACEHOLDERS.adoc+` in `+rsr-template-repo+`. diff --git a/REQUIRES_INITIALISATION.md b/REQUIRES_INITIALISATION.md deleted file mode 100644 index 47b6f8f..0000000 --- a/REQUIRES_INITIALISATION.md +++ /dev/null @@ -1,119 +0,0 @@ - - -# REQUIRES INITIALISATION - -**This repository is not finished being set up.** 9 substitution token(s) across 6 file(s) still have no value. - -## Why this is not already done - -This repo was created from `hyperpolymath/rsr-template-repo`. The mint -(`just repo-init`) fills every token that has a single mechanical answer — -owner, repo, author, dates, licence, branch — and it has done so here. - -The tokens below are the ones it *deliberately cannot* answer. They need a -decision or a fact that exists only in your head: what this project is for, -what command builds it, which port the service listens on, whether a PGP key -is held at all. The template's own token vocabulary says as much — you cannot -sensibly answer "required invariants" in a thirty-second bootstrap. - -They were left **visibly unfilled on purpose**. The alternatives were both -worse: inventing plausible values would put confident falsehoods into a -security policy and an architecture document, and silently deleting the -sections would hide the fact that a decision is owed. A visible gap is -honest; a fabricated answer is not. - -## Do not delete this file until every item below is resolved - -This file is the only marker that the work is outstanding. Deleting it early -does not finish the setup, it just conceals it — and the next person or agent -to arrive will reasonably assume the repo is complete. - -- **If you are a person:** delete this file yourself once the last item is done. -- **If you are an agent:** resolve what you legitimately can, leave the rest, - and delete this file only when no token below remains anywhere in the tree. - Do not delete it to make a gate go green. - -Re-running the estate top-up tool will remove this file automatically once -nothing is outstanding, so the safest way to finish is to fix the tokens and -let the check confirm it. - -## What is needed, and where it goes - -### `{{BUILD_CMD}}` - -The exact command that builds this project. - -Appears in: - -- `QUICKSTART-DEV.adoc` - -### `{{BUILD_OUTPUT_PATH}}` - -Where the build artefact lands. - -Appears in: - -- `QUICKSTART-MAINTAINER.adoc` - -### `{{DEPS}}` - -Prose summary of runtime/build dependencies. - -Appears in: - -- `QUICKSTART-MAINTAINER.adoc` - -### `{{LANG_STACK}}` - -The language stack, in prose. - -Appears in: - -- `QUICKSTART-DEV.adoc` - -### `{{MUST_INVARIANTS}}` - -The invariants this project guarantees. Not answerable in a bootstrap; it is the point of the repo. - -Appears in: - -- `QUICKSTART-DEV.adoc` - -### `{{PROJECT_UNIQUE_STRENGTH}}` - -What this does that its alternatives do not. - -Appears in: - -- `.machine_readable/bot_directives/methodology.a2ml` -- `.machine_readable/svc/k9/methodology-guard.k9.ncl` - -### `{{QUERY}}` - -Appears in: - -- `.machine_readable/contractiles/Justfile` -- `Justfile` - -### `{{TEST_CMD}}` - -The exact command that runs its tests. - -Appears in: - -- `QUICKSTART-DEV.adoc` - -### `{{VERSION}}` - -Version/tag for the container image. - -Appears in: - -- `.machine_readable/contractiles/Justfile` -- `Justfile` - ---- - -Generated by the estate top-up pass. Rationale and the governing rulings are -in `hyperpolymath/standards`; the token vocabulary is -`.machine_readable/ai/PLACEHOLDERS.adoc` in `rsr-template-repo`. diff --git a/SECURITY.adoc b/SECURITY.adoc new file mode 100644 index 0000000..6833c54 --- /dev/null +++ b/SECURITY.adoc @@ -0,0 +1,378 @@ +Security Policy + +We take security seriously. We appreciate your efforts to responsibly +disclose vulnerabilities and will make every effort to acknowledge your +contributions. Table of Contents + +.... +Reporting a Vulnerability +What to Include +Response Timeline +Disclosure Policy +Scope +Safe Harbour +Recognition +Security Updates +Security Best Practices +.... + +Reporting a Vulnerability Preferred Method: GitHub Security Advisories + +The preferred method for reporting security vulnerabilities is through +GitHub’s Security Advisory feature: + +.... +Navigate to Report a Vulnerability +Click "Report a vulnerability" +Complete the form with as much detail as possible +Submit — we'll receive a private notification +.... + +This method ensures: + +.... +End-to-end encryption of your report +Private discussion space for collaboration +Coordinated disclosure tooling +Automatic credit when the advisory is published +.... + +Alternative: Encrypted Email + +If you cannot use GitHub Security Advisories, you may email us directly: + +Email security@hyperpolymath.org PGP Key Download Public Key Fingerprint +See GPG key + +== Import our PGP key + +curl -sSL https://hyperpolymath.org/gpg/security.asc | gpg –import + +== Verify fingerprint + +gpg –fingerprint security@hyperpolymath.org + +== Encrypt your report + +gpg –armor –encrypt –recipient security@hyperpolymath.org report.txt + +.... +⚠️ Important: Do not report security vulnerabilities through public GitHub issues, pull requests, discussions, or social media. +.... + +What to Include + +A good vulnerability report helps us understand and reproduce the issue +quickly. Required Information + +.... +Description: Clear explanation of the vulnerability +Impact: What an attacker could achieve (confidentiality, integrity, availability) +Affected versions: Which versions/commits are affected +Reproduction steps: Detailed steps to reproduce the issue +.... + +Helpful Additional Information + +.... +Proof of concept: Code, scripts, or screenshots demonstrating the vulnerability +Attack scenario: Realistic attack scenario showing exploitability +CVSS score: Your assessment of severity (use CVSS 3.1 Calculator) +CWE ID: Common Weakness Enumeration identifier if known +Suggested fix: If you have ideas for remediation +References: Links to related vulnerabilities, research, or advisories +.... + +Example Report Structure + +=== Summary + +{empty}[One-sentence description of the vulnerability] + +=== Vulnerability Type + +{empty}[e.g., SQL Injection, XSS, SSRF, Path Traversal, etc.] + +=== Affected Component + +{empty}[File path, function name, API endpoint, etc.] + +=== Affected Versions + +{empty}[Version range or specific commits] + +=== Severity Assessment + +* CVSS 3.1 Score: [X.X] +* CVSS Vector: [CVSS:3.1/AV:X/AC:X/PR:X/UI:X/S:X/C:X/I:X/A:X] + +=== Description + +{empty}[Detailed technical description] + +=== Steps to Reproduce + +[arabic] +. [First step] +. [Second step] +. […] + +=== Proof of Concept + +{empty}[Code, curl commands, screenshots, etc.] + +=== Impact + +{empty}[What can an attacker achieve?] + +=== Suggested Remediation + +{empty}[Optional: your ideas for fixing] + +=== References + +{empty}[Links to related issues, CVEs, research] + +Response Timeline + +We commit to the following response times: Stage Timeframe Description +Initial Response 48 hours We acknowledge receipt and confirm we’re +investigating Triage 7 days We assess severity, confirm the +vulnerability, and estimate timeline Status Update Every 7 days Regular +updates on remediation progress Resolution 90 days Target for fix +development and release (complex issues may take longer) Disclosure 90 +days Public disclosure after fix is available (coordinated with you) + +.... +Note: These are targets, not guarantees. Complex vulnerabilities may require more time. We'll communicate openly about any delays. +.... + +Disclosure Policy + +We follow coordinated disclosure (also known as responsible disclosure): + +.... +You report the vulnerability privately +We acknowledge and begin investigation +We develop a fix and prepare a release +We coordinate disclosure timing with you +We publish security advisory and fix simultaneously +You may publish your research after disclosure +.... + +Our Commitments + +.... +We will not take legal action against researchers who follow this policy +We will work with you to understand and resolve the issue +We will credit you in the security advisory (unless you prefer anonymity) +We will notify you before public disclosure +We will publish advisories with sufficient detail for users to assess risk +.... + +Your Commitments + +.... +Report vulnerabilities promptly after discovery +Give us reasonable time to address the issue before disclosure +Do not access, modify, or delete data beyond what's necessary to demonstrate the vulnerability +Do not degrade service availability (no DoS testing on production) +Do not share vulnerability details with others until coordinated disclosure +.... + +Disclosure Timeline + +Day 0 You report vulnerability Day 1-2 We acknowledge receipt Day 7 We +confirm vulnerability and share initial assessment Day 7-90 We develop +and test fix Day 90 Coordinated public disclosure (earlier if fix is +ready; later by mutual agreement) + +If we cannot reach agreement on disclosure timing, we default to 90 days +from your initial report. Scope In Scope ✅ + +The following are within scope for security research: + +.... +This repository (hyperpolymath/terrapin-ssg) and all its code +Official releases and packages published from this repository +Documentation that could lead to security issues +Build and deployment configurations in this repository +Dependencies (report here, we'll coordinate with upstream) +.... + +Out of Scope ❌ + +The following are not in scope: + +.... +Third-party services we integrate with (report directly to them) +Social engineering attacks against maintainers +Physical security +Denial of service attacks against production infrastructure +Spam, phishing, or other non-technical attacks +Issues already reported or publicly known +Theoretical vulnerabilities without proof of concept +.... + +Qualifying Vulnerabilities + +We’re particularly interested in: + +.... +Remote code execution +SQL injection, command injection, code injection +Authentication/authorisation bypass +Cross-site scripting (XSS) and cross-site request forgery (CSRF) +Server-side request forgery (SSRF) +Path traversal / local file inclusion +Information disclosure (credentials, PII, secrets) +Cryptographic weaknesses +Deserialisation vulnerabilities +Memory safety issues (buffer overflows, use-after-free, etc.) +Supply chain vulnerabilities (dependency confusion, etc.) +Significant logic flaws +.... + +Non-Qualifying Issues + +The following generally do not qualify as security vulnerabilities: + +.... +Missing security headers on non-sensitive pages +Clickjacking on pages without sensitive actions +Self-XSS (requires victim to paste code) +Missing rate limiting (unless it enables a specific attack) +Username/email enumeration (unless high-risk context) +Missing cookie flags on non-sensitive cookies +Software version disclosure +Verbose error messages (unless exposing secrets) +Best practice deviations without demonstrable impact +.... + +Safe Harbour + +We support security research conducted in good faith. Our Promise + +If you conduct security research in accordance with this policy: + +.... +✅ We will not initiate legal action against you +✅ We will not report your activity to law enforcement +✅ We will work with you in good faith to resolve issues +✅ We consider your research authorised under the Computer Fraud and Abuse Act (CFAA), UK Computer Misuse Act, and similar laws +✅ We waive any potential claim against you for circumvention of security controls +.... + +Good Faith Requirements + +To qualify for safe harbour, you must: + +.... +Comply with this security policy +Report vulnerabilities promptly +Avoid privacy violations (do not access others' data) +Avoid service degradation (no destructive testing) +Not exploit vulnerabilities beyond proof-of-concept +Not use vulnerabilities for profit (beyond bug bounties where offered) + +⚠️ Important: This safe harbour does not extend to third-party systems. Always check their policies before testing. +.... + +Recognition + +We believe in recognising security researchers who help us improve. Hall +of Fame + +Researchers who report valid vulnerabilities will be acknowledged in our +Security Acknowledgments (unless they prefer anonymity). + +Recognition includes: + +.... +Your name (or chosen alias) +Link to your website/profile (optional) +Brief description of the vulnerability class +Date of report +.... + +What We Offer + +.... +✅ Public credit in security advisories +✅ Acknowledgment in release notes +✅ Entry in our Hall of Fame +✅ Reference/recommendation letter upon request (for significant findings) +.... + +What We Don’t Currently Offer + +.... +❌ Monetary bug bounties +❌ Hardware or swag +❌ Paid security research contracts + +Note: We're a community project with limited resources. Your contributions help everyone who uses this software. +.... + +Security Updates Receiving Updates + +To stay informed about security updates: + +.... +Watch this repository: Click "Watch" → "Custom" → Select "Security alerts" +GitHub Security Advisories: Published at Security Advisories +Release notes: Security fixes noted in CHANGELOG +.... + +Update Policy Severity Response Critical/High Patch release as soon as +fix is ready Medium Included in next scheduled release (or earlier) Low +Included in next scheduled release Supported Versions Version Supported +Notes main branch ✅ Yes Latest development Latest release ✅ Yes +Current stable Previous minor release ✅ Yes Security fixes backported +Older versions ❌ No Please upgrade Security Best Practices + +When using terrapin-ssg, we recommend: General + +.... +Keep dependencies up to date +Use the latest stable release +Subscribe to security notifications +Review configuration against security documentation +Follow principle of least privilege +.... + +For Contributors + +.... +Never commit secrets, credentials, or API keys +Use signed commits (git config commit.gpgsign true) +Review dependencies before adding them +Run security linters locally before pushing +Report any concerns about existing code +.... + +Additional Resources + +.... +Our PGP Public Key +Security Advisories +Changelog +Contributing Guidelines +CVE Database +CVSS Calculator +.... + +Contact Purpose Contact Security issues Report via GitHub or +security@hyperpolymath.org General questions GitHub Discussions Other +enquiries See README for contact information Policy Changes + +This security policy may be updated from time to time. Significant +changes will be: + +.... +Committed to this repository with a clear commit message +Noted in the changelog +Announced via GitHub Discussions (for major changes) +.... + +Thank you for helping keep terrapin-ssg and its users safe. diff --git a/SECURITY.md b/SECURITY.md deleted file mode 100644 index 762bf01..0000000 --- a/SECURITY.md +++ /dev/null @@ -1,332 +0,0 @@ - -Security Policy - -We take security seriously. We appreciate your efforts to responsibly disclose vulnerabilities and will make every effort to acknowledge your contributions. -Table of Contents - - Reporting a Vulnerability - What to Include - Response Timeline - Disclosure Policy - Scope - Safe Harbour - Recognition - Security Updates - Security Best Practices - -Reporting a Vulnerability -Preferred Method: GitHub Security Advisories - -The preferred method for reporting security vulnerabilities is through GitHub's Security Advisory feature: - - Navigate to Report a Vulnerability - Click "Report a vulnerability" - Complete the form with as much detail as possible - Submit — we'll receive a private notification - -This method ensures: - - End-to-end encryption of your report - Private discussion space for collaboration - Coordinated disclosure tooling - Automatic credit when the advisory is published - -Alternative: Encrypted Email - -If you cannot use GitHub Security Advisories, you may email us directly: - -Email security@hyperpolymath.org -PGP Key Download Public Key -Fingerprint See GPG key - -# Import our PGP key -curl -sSL https://hyperpolymath.org/gpg/security.asc | gpg --import - -# Verify fingerprint -gpg --fingerprint security@hyperpolymath.org - -# Encrypt your report -gpg --armor --encrypt --recipient security@hyperpolymath.org report.txt - - ⚠️ Important: Do not report security vulnerabilities through public GitHub issues, pull requests, discussions, or social media. - -What to Include - -A good vulnerability report helps us understand and reproduce the issue quickly. -Required Information - - Description: Clear explanation of the vulnerability - Impact: What an attacker could achieve (confidentiality, integrity, availability) - Affected versions: Which versions/commits are affected - Reproduction steps: Detailed steps to reproduce the issue - -Helpful Additional Information - - Proof of concept: Code, scripts, or screenshots demonstrating the vulnerability - Attack scenario: Realistic attack scenario showing exploitability - CVSS score: Your assessment of severity (use CVSS 3.1 Calculator) - CWE ID: Common Weakness Enumeration identifier if known - Suggested fix: If you have ideas for remediation - References: Links to related vulnerabilities, research, or advisories - -Example Report Structure - -## Summary -[One-sentence description of the vulnerability] - -## Vulnerability Type -[e.g., SQL Injection, XSS, SSRF, Path Traversal, etc.] - -## Affected Component -[File path, function name, API endpoint, etc.] - -## Affected Versions -[Version range or specific commits] - -## Severity Assessment -- CVSS 3.1 Score: [X.X] -- CVSS Vector: [CVSS:3.1/AV:X/AC:X/PR:X/UI:X/S:X/C:X/I:X/A:X] - -## Description -[Detailed technical description] - -## Steps to Reproduce -1. [First step] -2. [Second step] -3. [...] - -## Proof of Concept -[Code, curl commands, screenshots, etc.] - -## Impact -[What can an attacker achieve?] - -## Suggested Remediation -[Optional: your ideas for fixing] - -## References -[Links to related issues, CVEs, research] - -Response Timeline - -We commit to the following response times: -Stage Timeframe Description -Initial Response 48 hours We acknowledge receipt and confirm we're investigating -Triage 7 days We assess severity, confirm the vulnerability, and estimate timeline -Status Update Every 7 days Regular updates on remediation progress -Resolution 90 days Target for fix development and release (complex issues may take longer) -Disclosure 90 days Public disclosure after fix is available (coordinated with you) - - Note: These are targets, not guarantees. Complex vulnerabilities may require more time. We'll communicate openly about any delays. - -Disclosure Policy - -We follow coordinated disclosure (also known as responsible disclosure): - - You report the vulnerability privately - We acknowledge and begin investigation - We develop a fix and prepare a release - We coordinate disclosure timing with you - We publish security advisory and fix simultaneously - You may publish your research after disclosure - -Our Commitments - - We will not take legal action against researchers who follow this policy - We will work with you to understand and resolve the issue - We will credit you in the security advisory (unless you prefer anonymity) - We will notify you before public disclosure - We will publish advisories with sufficient detail for users to assess risk - -Your Commitments - - Report vulnerabilities promptly after discovery - Give us reasonable time to address the issue before disclosure - Do not access, modify, or delete data beyond what's necessary to demonstrate the vulnerability - Do not degrade service availability (no DoS testing on production) - Do not share vulnerability details with others until coordinated disclosure - -Disclosure Timeline - -Day 0 You report vulnerability -Day 1-2 We acknowledge receipt -Day 7 We confirm vulnerability and share initial assessment -Day 7-90 We develop and test fix -Day 90 Coordinated public disclosure - (earlier if fix is ready; later by mutual agreement) - -If we cannot reach agreement on disclosure timing, we default to 90 days from your initial report. -Scope -In Scope ✅ - -The following are within scope for security research: - - This repository (hyperpolymath/terrapin-ssg) and all its code - Official releases and packages published from this repository - Documentation that could lead to security issues - Build and deployment configurations in this repository - Dependencies (report here, we'll coordinate with upstream) - -Out of Scope ❌ - -The following are not in scope: - - Third-party services we integrate with (report directly to them) - Social engineering attacks against maintainers - Physical security - Denial of service attacks against production infrastructure - Spam, phishing, or other non-technical attacks - Issues already reported or publicly known - Theoretical vulnerabilities without proof of concept - -Qualifying Vulnerabilities - -We're particularly interested in: - - Remote code execution - SQL injection, command injection, code injection - Authentication/authorisation bypass - Cross-site scripting (XSS) and cross-site request forgery (CSRF) - Server-side request forgery (SSRF) - Path traversal / local file inclusion - Information disclosure (credentials, PII, secrets) - Cryptographic weaknesses - Deserialisation vulnerabilities - Memory safety issues (buffer overflows, use-after-free, etc.) - Supply chain vulnerabilities (dependency confusion, etc.) - Significant logic flaws - -Non-Qualifying Issues - -The following generally do not qualify as security vulnerabilities: - - Missing security headers on non-sensitive pages - Clickjacking on pages without sensitive actions - Self-XSS (requires victim to paste code) - Missing rate limiting (unless it enables a specific attack) - Username/email enumeration (unless high-risk context) - Missing cookie flags on non-sensitive cookies - Software version disclosure - Verbose error messages (unless exposing secrets) - Best practice deviations without demonstrable impact - -Safe Harbour - -We support security research conducted in good faith. -Our Promise - -If you conduct security research in accordance with this policy: - - ✅ We will not initiate legal action against you - ✅ We will not report your activity to law enforcement - ✅ We will work with you in good faith to resolve issues - ✅ We consider your research authorised under the Computer Fraud and Abuse Act (CFAA), UK Computer Misuse Act, and similar laws - ✅ We waive any potential claim against you for circumvention of security controls - -Good Faith Requirements - -To qualify for safe harbour, you must: - - Comply with this security policy - Report vulnerabilities promptly - Avoid privacy violations (do not access others' data) - Avoid service degradation (no destructive testing) - Not exploit vulnerabilities beyond proof-of-concept - Not use vulnerabilities for profit (beyond bug bounties where offered) - - ⚠️ Important: This safe harbour does not extend to third-party systems. Always check their policies before testing. - -Recognition - -We believe in recognising security researchers who help us improve. -Hall of Fame - -Researchers who report valid vulnerabilities will be acknowledged in our Security Acknowledgments (unless they prefer anonymity). - -Recognition includes: - - Your name (or chosen alias) - Link to your website/profile (optional) - Brief description of the vulnerability class - Date of report - -What We Offer - - ✅ Public credit in security advisories - ✅ Acknowledgment in release notes - ✅ Entry in our Hall of Fame - ✅ Reference/recommendation letter upon request (for significant findings) - -What We Don't Currently Offer - - ❌ Monetary bug bounties - ❌ Hardware or swag - ❌ Paid security research contracts - - Note: We're a community project with limited resources. Your contributions help everyone who uses this software. - -Security Updates -Receiving Updates - -To stay informed about security updates: - - Watch this repository: Click "Watch" → "Custom" → Select "Security alerts" - GitHub Security Advisories: Published at Security Advisories - Release notes: Security fixes noted in CHANGELOG - -Update Policy -Severity Response -Critical/High Patch release as soon as fix is ready -Medium Included in next scheduled release (or earlier) -Low Included in next scheduled release -Supported Versions -Version Supported Notes -main branch ✅ Yes Latest development -Latest release ✅ Yes Current stable -Previous minor release ✅ Yes Security fixes backported -Older versions ❌ No Please upgrade -Security Best Practices - -When using terrapin-ssg, we recommend: -General - - Keep dependencies up to date - Use the latest stable release - Subscribe to security notifications - Review configuration against security documentation - Follow principle of least privilege - -For Contributors - - Never commit secrets, credentials, or API keys - Use signed commits (git config commit.gpgsign true) - Review dependencies before adding them - Run security linters locally before pushing - Report any concerns about existing code - -Additional Resources - - Our PGP Public Key - Security Advisories - Changelog - Contributing Guidelines - CVE Database - CVSS Calculator - -Contact -Purpose Contact -Security issues Report via GitHub or security@hyperpolymath.org -General questions GitHub Discussions -Other enquiries See README for contact information -Policy Changes - -This security policy may be updated from time to time. Significant changes will be: - - Committed to this repository with a clear commit message - Noted in the changelog - Announced via GitHub Discussions (for major changes) - -Thank you for helping keep terrapin-ssg and its users safe. diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc new file mode 100644 index 0000000..f3f8e58 --- /dev/null +++ b/TEST-NEEDS.adoc @@ -0,0 +1,140 @@ +== TEST-NEEDS.md — nextgen-languages + +____ +Generated 2026-03-29 by punishing audit. +____ + +=== CRG Grade: C — ACHIEVED 2026-04-04 + +[width="100%",cols="47%,25%,28%",options="header",] +|=== +|Sub-project |Tests |Status +|ephapax (Rust workspace) |330 |CRG C complete 2026-04-04 + +|tangle (OCaml) |94 |Existing coverage adequate + +|affinescript (OCaml) |64 tested (22 pre-existing failures) +|Pre-existing, not regressions +|=== + +Added test categories for ephapax-linear and ephapax-lexer: - P2P +property tests: loop-based invariant checks (20+ iterations each) - E2E +tests: full pipeline tests (lexer->tokens, module->discipline check) - +Aspect tests: robustness, statelessness, edge cases, crash resistance + +=== Current State + +[width="100%",cols="50%,25%,25%",options="header",] +|=== +|Category |Count |Notes +|Unit tests |~50 |affinescript: test_lexer.ml, test_golden.ml, +test_e2e.ml + ~119 .as test files (borrow, codegen). tangle: +test_parser.ml, test_typecheck.ml, test_eval.ml + +|Integration |~5 |tangle FFI integration_test.zig, ephapax tests.rs +(per-language suites live in each language’s own repo) + +|E2E |~3 |affinescript test_e2e.ml + integration tests + +|Benchmarks |4 |tangle: bench_lexer.ml, bench_lexer.rs, bench_parser.ml, +bench_parser_rust.rs. betlang: bench_lexer.rs +|=== + +*Source modules:* ~772 across the family’s language implementations. +Major: affinescript (~87 ML), ephapax (~488 Rust across 19 crates), +tangle, eclexia, betlang, anvomidav, wokelang, error-lang, jtv. (Counts +predate the pure-coordinator pivot; the code now lives in each +language’s own repo — treat as historical.) + +=== What’s Missing + +==== P2P (Property-Based) Tests + +* [ ] affinescript: borrow checker property tests (arbitrary program +shapes) +* [ ] ephapax: linear type checker property tests — CRITICAL (19 crates, +only tests.rs) +* [ ] tangle: parser roundtrip property tests +* [ ] All languages: lexer/parser fuzzing for crash resistance + +==== E2E Tests + +* [ ] Each language: source -> lex -> parse -> typecheck -> codegen -> +execute +* [ ] affinescript: full compile pipeline with borrow checking +* [ ] ephapax: full linear type checking pipeline (19 crates, needs +integration) +* [ ] tangle: full compilation to target +* [ ] Cross-language: shared concepts verified across implementations + +==== Aspect Tests + +* *Security:* No tests for code injection through language constructs, +unsafe memory in codegen, sandbox escape in interpreters +* *Performance:* tangle has lexer/parser benchmarks (good). +affinescript: ZERO benchmarks. ephapax: ZERO benchmarks for 19 crates +* *Concurrency:* No tests for parallel compilation, concurrent type +checking +* *Error handling:* affinescript has test files for error cases (good). +Most other languages: ZERO error handling tests + +==== Build & Execution + +* [ ] OCaml build + test for affinescript, tangle +* [ ] `+cargo test+` for ephapax (19 crates!) +* [ ] Zig build for tangle FFI +* [ ] Test runners for each language + +==== Benchmarks Needed + +* [ ] ephapax: type checking time, compilation time, memory usage (19 +crates, ZERO benchmarks) +* [ ] affinescript: compilation pipeline benchmarks +* [ ] eclexia: parsing/evaluation benchmarks +* [ ] All languages: parse time vs source size + +==== Self-Tests + +* [ ] Each language: self-hosting test (can it compile its own test +suite?) +* [ ] Grammar consistency checks +* [ ] Type system soundness verification + +==== CRITICAL GAPS + +[width="100%",cols="27%,34%,18%,21%",options="header",] +|=== +|Language |Source Files |Tests |Status +|affinescript |~87 ML |~50 unit + 119 .as |*Good coverage* +|ephapax |~488 Rust (19 crates) |1 tests.rs |*0.2% — CATASTROPHIC* +|tangle |moderate |3 ML + 1 Zig + 4 bench |Adequate for size +|eclexia |unknown |0 |*Untested* +|betlang |unknown |1 bench |*Untested* +|anvomidav |unknown |0 |*Untested* +|wokelang |unknown |0 |*Untested* +|error-lang |unknown |0 |*Untested* +|jtv |unknown |0 |*Untested* +|=== + +____ +Note: `+tentacles-agentic-syllabus+` (formerly _7-tentacles_) is the +curriculum framework, *not* a language (see `+0-AI-MANIFEST.a2ml+` §6). +Its test posture is tracked in its own repo and is intentionally +excluded from this per-language table. +____ + +=== Priority + +*CRITICAL.* Ephapax at 488 Rust source files across 19 crates with +effectively 1 test file is catastrophic — this is a compiler with linear +types that needs rigorous testing above all else. affinescript is the +only well-tested language. At least 6 language implementations have ZERO +tests. The tangle benchmarks are a good model for the rest. + +=== FAKE-FUZZ ALERT + +* `+tests/fuzz/placeholder.txt+` is a scorecard placeholder inherited +from rsr-template-repo — it does NOT provide real fuzz testing +* Replace with an actual fuzz harness (see +rsr-template-repo/tests/fuzz/README.adoc) or remove the file +* Priority: P2 — creates false impression of fuzz coverage diff --git a/TEST-NEEDS.md b/TEST-NEEDS.md deleted file mode 100644 index 083fdf4..0000000 --- a/TEST-NEEDS.md +++ /dev/null @@ -1,97 +0,0 @@ - -# TEST-NEEDS.md — nextgen-languages - -> Generated 2026-03-29 by punishing audit. - -## CRG Grade: C — ACHIEVED 2026-04-04 - -| Sub-project | Tests | Status | -|-------------|-------|--------| -| ephapax (Rust workspace) | 330 | CRG C complete 2026-04-04 | -| tangle (OCaml) | 94 | Existing coverage adequate | -| affinescript (OCaml) | 64 tested (22 pre-existing failures) | Pre-existing, not regressions | - -Added test categories for ephapax-linear and ephapax-lexer: -- P2P property tests: loop-based invariant checks (20+ iterations each) -- E2E tests: full pipeline tests (lexer->tokens, module->discipline check) -- Aspect tests: robustness, statelessness, edge cases, crash resistance - -## Current State - -| Category | Count | Notes | -|-------------|-------|-------| -| Unit tests | ~50 | affinescript: test_lexer.ml, test_golden.ml, test_e2e.ml + ~119 .as test files (borrow, codegen). tangle: test_parser.ml, test_typecheck.ml, test_eval.ml | -| Integration | ~5 | tangle FFI integration_test.zig, ephapax tests.rs (per-language suites live in each language's own repo) | -| E2E | ~3 | affinescript test_e2e.ml + integration tests | -| Benchmarks | 4 | tangle: bench_lexer.ml, bench_lexer.rs, bench_parser.ml, bench_parser_rust.rs. betlang: bench_lexer.rs | - -**Source modules:** ~772 across the family's language implementations. Major: affinescript (~87 ML), ephapax (~488 Rust across 19 crates), tangle, eclexia, betlang, anvomidav, wokelang, error-lang, jtv. (Counts predate the pure-coordinator pivot; the code now lives in each language's own repo — treat as historical.) - -## What's Missing - -### P2P (Property-Based) Tests -- [ ] affinescript: borrow checker property tests (arbitrary program shapes) -- [ ] ephapax: linear type checker property tests — CRITICAL (19 crates, only tests.rs) -- [ ] tangle: parser roundtrip property tests -- [ ] All languages: lexer/parser fuzzing for crash resistance - -### E2E Tests -- [ ] Each language: source -> lex -> parse -> typecheck -> codegen -> execute -- [ ] affinescript: full compile pipeline with borrow checking -- [ ] ephapax: full linear type checking pipeline (19 crates, needs integration) -- [ ] tangle: full compilation to target -- [ ] Cross-language: shared concepts verified across implementations - -### Aspect Tests -- **Security:** No tests for code injection through language constructs, unsafe memory in codegen, sandbox escape in interpreters -- **Performance:** tangle has lexer/parser benchmarks (good). affinescript: ZERO benchmarks. ephapax: ZERO benchmarks for 19 crates -- **Concurrency:** No tests for parallel compilation, concurrent type checking -- **Error handling:** affinescript has test files for error cases (good). Most other languages: ZERO error handling tests - -### Build & Execution -- [ ] OCaml build + test for affinescript, tangle -- [ ] `cargo test` for ephapax (19 crates!) -- [ ] Zig build for tangle FFI -- [ ] Test runners for each language - -### Benchmarks Needed -- [ ] ephapax: type checking time, compilation time, memory usage (19 crates, ZERO benchmarks) -- [ ] affinescript: compilation pipeline benchmarks -- [ ] eclexia: parsing/evaluation benchmarks -- [ ] All languages: parse time vs source size - -### Self-Tests -- [ ] Each language: self-hosting test (can it compile its own test suite?) -- [ ] Grammar consistency checks -- [ ] Type system soundness verification - -### CRITICAL GAPS - -| Language | Source Files | Tests | Status | -|----------|-------------|-------|--------| -| affinescript | ~87 ML | ~50 unit + 119 .as | **Good coverage** | -| ephapax | ~488 Rust (19 crates) | 1 tests.rs | **0.2% — CATASTROPHIC** | -| tangle | moderate | 3 ML + 1 Zig + 4 bench | Adequate for size | -| eclexia | unknown | 0 | **Untested** | -| betlang | unknown | 1 bench | **Untested** | -| anvomidav | unknown | 0 | **Untested** | -| wokelang | unknown | 0 | **Untested** | -| error-lang | unknown | 0 | **Untested** | -| jtv | unknown | 0 | **Untested** | - -> Note: `tentacles-agentic-syllabus` (formerly *7-tentacles*) is the curriculum framework, -> **not** a language (see `0-AI-MANIFEST.a2ml` §6). Its test posture is tracked in its own -> repo and is intentionally excluded from this per-language table. - -## Priority - -**CRITICAL.** Ephapax at 488 Rust source files across 19 crates with effectively 1 test file is catastrophic — this is a compiler with linear types that needs rigorous testing above all else. affinescript is the only well-tested language. At least 6 language implementations have ZERO tests. The tangle benchmarks are a good model for the rest. - -## FAKE-FUZZ ALERT - -- `tests/fuzz/placeholder.txt` is a scorecard placeholder inherited from rsr-template-repo — it does NOT provide real fuzz testing -- Replace with an actual fuzz harness (see rsr-template-repo/tests/fuzz/README.adoc) or remove the file -- Priority: P2 — creates false impression of fuzz coverage diff --git a/TOPOLOGY.md b/TOPOLOGY.adoc similarity index 61% rename from TOPOLOGY.md rename to TOPOLOGY.adoc index 2f23d16..ee1a277 100644 --- a/TOPOLOGY.md +++ b/TOPOLOGY.adoc @@ -1,20 +1,14 @@ - - - +== Next-Gen Languages — Coordinator Topology -# Next-Gen Languages — Coordinator Topology +`+nextgen-languages+` is a *pure coordinator*. It contains no language +code: it _references_ a family of standalone `+hyperpolymath/+` +repositories and holds the cross-language registries, trackers, +governance, and CI that coordinate them. The map below is a reference +diagram, *not* an in-tree component tree. -`nextgen-languages` is a **pure coordinator**. It contains no language code: it -*references* a family of standalone `hyperpolymath/` repositories and holds the -cross-language registries, trackers, governance, and CI that coordinate them. The map -below is a reference diagram, **not** an in-tree component tree. +=== Reference map -## Reference map - -``` +.... ┌───────────────────────────────────────────────┐ │ nextgen-languages (this repo) │ │ PURE COORDINATOR │ @@ -47,31 +41,39 @@ below is a reference diagram, **not** an in-tree component tree. │ error-lang │ │ tangle │ └────────────────┘ -``` +.... -## Adjacent estates (referenced, out of scope) +=== Adjacent estates (referenced, out of scope) -Tracked elsewhere and listed only for discoverability — **not** part of the language-family -registry: the KRL resolution stack (`krl → TangleIR → VeriSimCore → Skein.jl / quandledb`) -and the database / type-theory languages (VCL-total, Quandledb, TypeLL, PanLL, -VQL/GQL/FBQL-DT). See `docs/language-portfolio.md` and the "Adjacent estates" section of -`TOOLING-STATUS.adoc`. +Tracked elsewhere and listed only for discoverability — *not* part of +the language-family registry: the KRL resolution stack +(`+krl → TangleIR → VeriSimCore → Skein.jl / quandledb+`) and the +database / type-theory languages (VCL-total, Quandledb, TypeLL, PanLL, +VQL/GQL/FBQL-DT). See `+docs/language-portfolio.md+` and the "`Adjacent +estates`" section of `+TOOLING-STATUS.adoc+`. -## Where status actually lives +=== Where status actually lives -This coordinator does **not** assert per-language completion — maturity is tracked in each -language's own repo and mirrored in the canonical trackers: +This coordinator does *not* assert per-language completion — maturity is +tracked in each language’s own repo and mirrored in the canonical +trackers: -- `.machine_readable/LANGUAGES.a2ml` — machine-readable registry (id, repo, invariant, status) -- `TOOLING-STATUS.adoc` — per-language grade matrix (CRG/TRG/ARG/FRG/RSR) -- `PROOF-NEEDS.md` / `TEST-NEEDS.md` — cross-language proof/test gaps -- `language-status-tracker.jl` — script that reports cross-language repo status +* `+.machine_readable/LANGUAGES.a2ml+` — machine-readable registry (id, +repo, invariant, status) +* `+TOOLING-STATUS.adoc+` — per-language grade matrix +(CRG/TRG/ARG/FRG/RSR) +* `+PROOF-NEEDS.md+` / `+TEST-NEEDS.md+` — cross-language proof/test +gaps +* `+language-status-tracker.jl+` — script that reports cross-language +repo status -The coordinator's own scaffolding status lives in `.machine_readable/6a2/STATE.a2ml` -(`completion-percentage`), which reflects coordinator maturity — not a family-wide 100%. +The coordinator’s own scaffolding status lives in +`+.machine_readable/6a2/STATE.a2ml+` (`+completion-percentage+`), which +reflects coordinator maturity — not a family-wide 100%. -## Update protocol +=== Update protocol -When the family changes (a language added, extracted, renamed, or retired), update the -registries listed above **together** — they must agree — then refresh this map. Do not add -per-language implementation detail here; it belongs in that language's own repo. +When the family changes (a language added, extracted, renamed, or +retired), update the registries listed above *together* — they must +agree — then refresh this map. Do not add per-language implementation +detail here; it belongs in that language’s own repo. diff --git a/docs/disambiguation/ephapax-vs-affinescript.adoc b/docs/disambiguation/ephapax-vs-affinescript.adoc new file mode 100644 index 0000000..240c9de --- /dev/null +++ b/docs/disambiguation/ephapax-vs-affinescript.adoc @@ -0,0 +1,207 @@ +== Ephapax vs AffineScript — these are different languages + +____ +⚠️ *STOP.* If you arrived here because you were about to apply a lesson, +snippet, fact, or tactic learned in one of these two repos to the other +— *don’t*. They share zero source-level structure. The only thing in +common is the compile target. +____ + +=== The one-sentence rule + +*Ephapax* and *AffineScript* are two unrelated languages from the same +author. They both happen to use type systems with _affine-flavored_ +substructural properties — which is true of nearly every modern +resource-safe language — and the lexical overlap of the word "`affine`" +is the entire reason agents and humans confuse them. + +[width="100%",cols="34%,33%,33%",options="header",] +|=== +| |Ephapax |AffineScript +|*What it is* |Research language for compile-time WebAssembly memory +safety |Successor to JS / TypeScript / ReScript + +|*Repo* |`+hyperpolymath/ephapax+` |`+hyperpolymath/affinescript+` + +|*Audience* |Formal-methods researchers, systems verifiers |Application +developers, JS-ecosystem users + +|*Surface syntax* |`+.eph+` (Coq-like / ML-shaped) |`+.affine+`, plus +brand-faces: jaffascript / rattlescript / lucidscript / cafescripto / +pseudoscript + +|*AST/IR* |`+src/ephapax-syntax/src/lib.rs+`, `+src/ephapax-ir+` +|`+lib/ast.ml+`, `+lib/borrow.ml+` + +|*Type checker* |`+ephapax-linear/src/{linear,affine}.rs+` (Rust, dyadic +— see below) |`+lib/borrow.ml+` (OCaml, single discipline with +capabilities) + +|*Structural rule* |Linear (strict) + Affine (companion) — same AST, two +checkers |Affine with explicit borrow/copy/drop, NLL-style scopes + +|*Binding forms* |`+let-linear+`, `+region r in …+`, regions/exits +|`+let+`, `+borrow+`/`+copy+`/`+drop+`, no first-class regions + +|*Effects* |Region-typed; tracked in type system |Capabilities (`+io+`, +`+dom+`, `+pixi+`, `+tea+`, …); host-facing + +|*Compiler stack* |Cargo workspace; Rust + Idris2 + Coq |Dune project; +OCaml + ReScript runtime + +|*Codegen* |typed-wasm via `+src/ephapax-wasm+`, formal correctness +lemma WIP |typed-wasm via `+lib/tw_*.ml+`, plus Deno-ESM and Node-CJS +direct emit + +|*Faces / frontends* |None — one surface syntax |Many (jaffascript, +rattlescript, lucidscript, cafescripto, pseudoscript) — all desugar to +the same core + +|*Formal semantics* |Mechanized in Coq (`+formal/Semantics.v+`, +`+formal/Linearity.v+`) + Idris2 ABI (`+src/abi/Ephapax/…+`) +|Operational; soundness arguments in `+lib/borrow.ml+` comments + +`+docs/CAPABILITY-MATRIX.adoc+`; tracking via `+docs/TECH-DEBT.adoc+` +and issue #177 (CORE-01) + +|*Proof obligations* |`+formal/PRESERVATION-HANDOFF.md+`, +`+ROADMAP.adoc+` § "`Preservation closure plan`", PR ephapax#146 |None +mechanized; `+verification/proofs/+` dirs are RSR template scaffolding +only + +|*Standard library* |`+ephapax-linear/src/+`, `+examples/+` +|`+stdlib/+`, `+vendor/+`, bindings (`+affinescript-dom+`, +`+affinescript-pixijs+`, `+affinescript-tea+`) + +|*Editor support* |`+editors/+`, `+idris2/+` LSP work |`+vscode-ext/+`, +NPM-published `+@hyperpolymath/affine-vscode+` + +|*Status* |Research-active; preservation theorem in flight +|Application-active; multiple PRs/release cycle +|=== + +=== What is shared + +*Two things, both via `+hyperpolymath/typed-wasm+`:* + +[arabic] +. Both languages compile (or are moving towards compiling) to +typed-wasm. +. Both languages interface with the same Rust verifier crate +`+crates/typed-wasm-verify/+` inside the typed-wasm repo. + +That is the entire shared surface. They are *sibling languages standing +on a common verification substrate* — not an implementation ↔ proof +pair, not a parent ↔ dialect pair, not a frontend ↔ backend pair. + +=== The dyadic-ephapax internal naming trap + +Ephapax is _itself_ dyadic. Inside the ephapax repo there are two +sublanguages: + +* *ephapax-linear* — the strict, formally-verified core. +* *ephapax-affine* — a more versatile prototyping companion that works +*with* ephapax-linear. + +Both are _ephapax-internal_. They share one AST, one Rust crate +(`+ephapax-linear/+`), one grammar directory +(`+ephapax-linear/grammar/{linear,affine}.ebnf+`). The "`affine`" in +"`ephapax-affine`" names the _structural discipline_ — one of two +type-checking modes in one crate. + +*ephapax-affine is NOT AffineScript.* The word `+affine+` overlapping in +both names is a coincidence of substructural-logic terminology, not a +relationship. AffineScript is a separate language with its own AST, its +own borrow checker, its own faces. + +=== Why the confusion happens + +Three traps stacked on each other: + +[arabic] +. *Lexical*: both names contain `+affine+`. +. *Conceptual*: both use type systems with affine-logic properties, +because nearly every resource-safe language does (Rust, Linear Haskell, +F*, Idris with QTT, Granule, …). The mere presence of "`affine`" in a +description is not a fingerprint. +. *Single-author*: both projects come from the same author, so +cross-references and shared idioms appear in commit messages, docs, and +chat. Don’t read those as evidence of structural relationship. + +=== How to tell which you’re in + +Quick visual signals, in priority order: + +[width="100%",cols="34%,33%,33%",options="header",] +|=== +|Signal |Ephapax |AffineScript +|Repo URL |`+github.com/hyperpolymath/ephapax+` +|`+github.com/hyperpolymath/affinescript+` + +|Build tool |`+Cargo.toml+` at root |`+dune-project+` at root + +|Main language |Rust (+ Coq + Idris2) |OCaml (+ ReScript runtime) + +|File extension under work |`+.eph+`, `+.v+`, `+.idr+` |`+.affine+`, +`+.ml+`, `+.res+` + +|Top-level dirs |`+formal/+`, `+idris2/+`, `+ephapax-linear/+`, `+src/+` +|`+lib/+`, `+vendor/+`, `+stdlib/+`, face-directories + +|Headline file |`+formal/Semantics.v+`, `+ROADMAP.adoc+` +|`+lib/borrow.ml+`, `+docs/CAPABILITY-MATRIX.adoc+` + +|Open soundness ticket |preservation 11 admits (Brief C / PR +ephapax#146) |issue affinescript#177 (CORE-01) +|=== + +If you can’t tell from the repo URL alone, you are in the wrong context +for the work. + +=== Specific guidance for AI agents + +*Do:* - When switching context between the two, state it explicitly: +"`switching context from AffineScript to ephapax`" (or vice versa). This +forces the user-visible audit trail. - Treat memory entries written +about one as inadmissible for the other unless the cross-reference is +explicit and recent. - When you read a snippet mentioning "`affine`", +look at _which file path_ it lives in before assuming you know which +language is meant. - Cross-reference the canonical disambiguation memory +entry: `+feedback_affinescript_ephapax_siblings_not_impl_proof.md+`. + +*Don’t:* - Apply borrow-checker tactics from `+lib/borrow.ml+` (OCaml, +AffineScript) to `+formal/Semantics.v+` (Coq, ephapax) or vice versa. - +Re-use proof-obligation framings across the two. Ephapax has Coq/Idris2 +mechanized proofs; AffineScript has compiler-correctness arguments. - +Conflate `+ephapax-affine+` (the sublanguage _inside_ ephapax) with +`+AffineScript+`. They have nothing in common beyond the syllable. - +Assume that a typed-wasm-side change in one repo implies anything about +the other. The verifier crate is shared, but the consumers are +independent. + +=== Cross-pointers + +* *Ephapax*: `+hyperpolymath/ephapax+` — README.adoc, ROADMAP.adoc, +formal/PRESERVATION-HANDOFF.md. +* *AffineScript*: `+hyperpolymath/affinescript+` — README.adoc, +docs/ECOSYSTEM.adoc, docs/CAPABILITY-MATRIX.adoc. +* *Shared target*: `+hyperpolymath/typed-wasm+` — README.adoc. Documents +both languages as independent producers. +* *Canonical disambiguation memory entry*: +`+feedback_affinescript_ephapax_siblings_not_impl_proof.md+` (in the +user’s auto-memory; durable across sessions). + +=== When this doc is wrong + +The canonical statement is the source code. If this doc and the source +disagree, update this doc. Keep the disambiguation specific and current: + +* If ephapax adds a third sublanguage, update the dyadic-naming-trap +section. +* If AffineScript adds a face, update the faces row in the comparison +table. +* If the two ever share more than typed-wasm + the Rust verifier, update +the "`What is shared`" section before anything else. +* If a new confusion class emerges (e.g., a third language with +`+affine+` in the name), extend this doc rather than fork. + +Last revised: 2026-05-26. diff --git a/docs/disambiguation/ephapax-vs-affinescript.md b/docs/disambiguation/ephapax-vs-affinescript.md deleted file mode 100644 index 1fd9b71..0000000 --- a/docs/disambiguation/ephapax-vs-affinescript.md +++ /dev/null @@ -1,109 +0,0 @@ - - - -# Ephapax vs AffineScript — these are different languages - -> ⚠️ **STOP.** If you arrived here because you were about to apply a lesson, snippet, fact, or tactic learned in one of these two repos to the other — **don't**. They share zero source-level structure. The only thing in common is the compile target. - -## The one-sentence rule - -**Ephapax** and **AffineScript** are two unrelated languages from the same author. They both happen to use type systems with *affine-flavored* substructural properties — which is true of nearly every modern resource-safe language — and the lexical overlap of the word "affine" is the entire reason agents and humans confuse them. - -| | Ephapax | AffineScript | -|---|---|---| -| **What it is** | Research language for compile-time WebAssembly memory safety | Successor to JS / TypeScript / ReScript | -| **Repo** | `hyperpolymath/ephapax` | `hyperpolymath/affinescript` | -| **Audience** | Formal-methods researchers, systems verifiers | Application developers, JS-ecosystem users | -| **Surface syntax** | `.eph` (Coq-like / ML-shaped) | `.affine`, plus brand-faces: jaffascript / rattlescript / lucidscript / cafescripto / pseudoscript | -| **AST/IR** | `src/ephapax-syntax/src/lib.rs`, `src/ephapax-ir` | `lib/ast.ml`, `lib/borrow.ml` | -| **Type checker** | `ephapax-linear/src/{linear,affine}.rs` (Rust, dyadic — see below) | `lib/borrow.ml` (OCaml, single discipline with capabilities) | -| **Structural rule** | Linear (strict) + Affine (companion) — same AST, two checkers | Affine with explicit borrow/copy/drop, NLL-style scopes | -| **Binding forms** | `let-linear`, `region r in …`, regions/exits | `let`, `borrow`/`copy`/`drop`, no first-class regions | -| **Effects** | Region-typed; tracked in type system | Capabilities (`io`, `dom`, `pixi`, `tea`, …); host-facing | -| **Compiler stack** | Cargo workspace; Rust + Idris2 + Coq | Dune project; OCaml + ReScript runtime | -| **Codegen** | typed-wasm via `src/ephapax-wasm`, formal correctness lemma WIP | typed-wasm via `lib/tw_*.ml`, plus Deno-ESM and Node-CJS direct emit | -| **Faces / frontends** | None — one surface syntax | Many (jaffascript, rattlescript, lucidscript, cafescripto, pseudoscript) — all desugar to the same core | -| **Formal semantics** | Mechanized in Coq (`formal/Semantics.v`, `formal/Linearity.v`) + Idris2 ABI (`src/abi/Ephapax/…`) | Operational; soundness arguments in `lib/borrow.ml` comments + `docs/CAPABILITY-MATRIX.adoc`; tracking via `docs/TECH-DEBT.adoc` and issue #177 (CORE-01) | -| **Proof obligations** | `formal/PRESERVATION-HANDOFF.md`, `ROADMAP.adoc` § "Preservation closure plan", PR ephapax#146 | None mechanized; `verification/proofs/` dirs are RSR template scaffolding only | -| **Standard library** | `ephapax-linear/src/`, `examples/` | `stdlib/`, `vendor/`, bindings (`affinescript-dom`, `affinescript-pixijs`, `affinescript-tea`) | -| **Editor support** | `editors/`, `idris2/` LSP work | `vscode-ext/`, NPM-published `@hyperpolymath/affine-vscode` | -| **Status** | Research-active; preservation theorem in flight | Application-active; multiple PRs/release cycle | - -## What is shared - -**Two things, both via `hyperpolymath/typed-wasm`:** - -1. Both languages compile (or are moving towards compiling) to typed-wasm. -2. Both languages interface with the same Rust verifier crate `crates/typed-wasm-verify/` inside the typed-wasm repo. - -That is the entire shared surface. They are **sibling languages standing on a common verification substrate** — not an implementation ↔ proof pair, not a parent ↔ dialect pair, not a frontend ↔ backend pair. - -## The dyadic-ephapax internal naming trap - -Ephapax is *itself* dyadic. Inside the ephapax repo there are two sublanguages: - -- **ephapax-linear** — the strict, formally-verified core. -- **ephapax-affine** — a more versatile prototyping companion that works **with** ephapax-linear. - -Both are *ephapax-internal*. They share one AST, one Rust crate (`ephapax-linear/`), one grammar directory (`ephapax-linear/grammar/{linear,affine}.ebnf`). The "affine" in "ephapax-affine" names the *structural discipline* — one of two type-checking modes in one crate. - -**ephapax-affine is NOT AffineScript.** The word `affine` overlapping in both names is a coincidence of substructural-logic terminology, not a relationship. AffineScript is a separate language with its own AST, its own borrow checker, its own faces. - -## Why the confusion happens - -Three traps stacked on each other: - -1. **Lexical**: both names contain `affine`. -2. **Conceptual**: both use type systems with affine-logic properties, because nearly every resource-safe language does (Rust, Linear Haskell, F*, Idris with QTT, Granule, …). The mere presence of "affine" in a description is not a fingerprint. -3. **Single-author**: both projects come from the same author, so cross-references and shared idioms appear in commit messages, docs, and chat. Don't read those as evidence of structural relationship. - -## How to tell which you're in - -Quick visual signals, in priority order: - -| Signal | Ephapax | AffineScript | -|---|---|---| -| Repo URL | `github.com/hyperpolymath/ephapax` | `github.com/hyperpolymath/affinescript` | -| Build tool | `Cargo.toml` at root | `dune-project` at root | -| Main language | Rust (+ Coq + Idris2) | OCaml (+ ReScript runtime) | -| File extension under work | `.eph`, `.v`, `.idr` | `.affine`, `.ml`, `.res` | -| Top-level dirs | `formal/`, `idris2/`, `ephapax-linear/`, `src/` | `lib/`, `vendor/`, `stdlib/`, face-directories | -| Headline file | `formal/Semantics.v`, `ROADMAP.adoc` | `lib/borrow.ml`, `docs/CAPABILITY-MATRIX.adoc` | -| Open soundness ticket | preservation 11 admits (Brief C / PR ephapax#146) | issue affinescript#177 (CORE-01) | - -If you can't tell from the repo URL alone, you are in the wrong context for the work. - -## Specific guidance for AI agents - -**Do:** -- When switching context between the two, state it explicitly: "switching context from AffineScript to ephapax" (or vice versa). This forces the user-visible audit trail. -- Treat memory entries written about one as inadmissible for the other unless the cross-reference is explicit and recent. -- When you read a snippet mentioning "affine", look at *which file path* it lives in before assuming you know which language is meant. -- Cross-reference the canonical disambiguation memory entry: `feedback_affinescript_ephapax_siblings_not_impl_proof.md`. - -**Don't:** -- Apply borrow-checker tactics from `lib/borrow.ml` (OCaml, AffineScript) to `formal/Semantics.v` (Coq, ephapax) or vice versa. -- Re-use proof-obligation framings across the two. Ephapax has Coq/Idris2 mechanized proofs; AffineScript has compiler-correctness arguments. -- Conflate `ephapax-affine` (the sublanguage *inside* ephapax) with `AffineScript`. They have nothing in common beyond the syllable. -- Assume that a typed-wasm-side change in one repo implies anything about the other. The verifier crate is shared, but the consumers are independent. - -## Cross-pointers - -- **Ephapax**: `hyperpolymath/ephapax` — README.adoc, ROADMAP.adoc, formal/PRESERVATION-HANDOFF.md. -- **AffineScript**: `hyperpolymath/affinescript` — README.adoc, docs/ECOSYSTEM.adoc, docs/CAPABILITY-MATRIX.adoc. -- **Shared target**: `hyperpolymath/typed-wasm` — README.adoc. Documents both languages as independent producers. -- **Canonical disambiguation memory entry**: `feedback_affinescript_ephapax_siblings_not_impl_proof.md` (in the user's auto-memory; durable across sessions). - -## When this doc is wrong - -The canonical statement is the source code. If this doc and the source disagree, update this doc. Keep the disambiguation specific and current: - -- If ephapax adds a third sublanguage, update the dyadic-naming-trap section. -- If AffineScript adds a face, update the faces row in the comparison table. -- If the two ever share more than typed-wasm + the Rust verifier, update the "What is shared" section before anything else. -- If a new confusion class emerges (e.g., a third language with `affine` in the name), extend this doc rather than fork. - -Last revised: 2026-05-26. diff --git a/docs/language-portfolio.adoc b/docs/language-portfolio.adoc new file mode 100644 index 0000000..06fdf24 --- /dev/null +++ b/docs/language-portfolio.adoc @@ -0,0 +1,103 @@ +== Hyperpolymath Language Portfolio + +*Last updated:* 2026-07-02 + +This is a cross-language index. `+nextgen-languages+` is a *pure +coordinator*: it does not contain any language. Each language is its own +standalone `+hyperpolymath/+` repo. *Per-language status, +completion, and tech-stack detail are not duplicated here* — they live +in each language’s own repo and in the coordinator’s canonical trackers: + +* *`+.machine_readable/LANGUAGES.a2ml+`* — the machine-readable language +registry +* *`+language-status-tracker.jl+`* — the script that computes +cross-language status +* *`+TOOLING-STATUS.adoc+`* — the per-language grade matrix +(CRG/TRG/ARG/FRG/RSR) +* *`+PROOF-NEEDS.md+` / `+TEST-NEEDS.md+`* — cross-language proof/test +gaps + +=== General-purpose languages + +[width="100%",cols="33%,19%,48%",options="header",] +|=== +|Language |Repo |One-line role +|Phronesis |`+hyperpolymath/phronesis+` |Formal, auditable agent ethics + +|Eclexia |`+hyperpolymath/eclexia+` |Resource-first / green computing + +|WokeLang |`+hyperpolymath/wokelang+` |Consent & well-being as +primitives + +|AffineScript |`+hyperpolymath/affinescript+` |Affine types targeting +WasmGC + +|Ephapax |`+hyperpolymath/ephapax+` |Dyadic linear/affine types → WasmGC + +|My-Lang |`+hyperpolymath/my-lang+` |Solo → Duet → Ensemble dialect +family + +|JtV |`+hyperpolymath/jtv+` |Systems language, Harvard architecture + +|Error-Lang |`+hyperpolymath/error-lang+` |Pedagogical, systems thinking +via errors + +|Haec |`+hyperpolymath/haec+` |Trope-particularity: graded +property-instance loss, use-checked + +|Oblíbený |`+hyperpolymath/oblibeny+` |Turing-incomplete secure +deployment + +|Anvomidav |`+hyperpolymath/anvomidav+` |Hard real-time / formal +verification + +|betlang |`+hyperpolymath/betlang+` |Foundational / probabilistic +experiment + +|Tangle |`+hyperpolymath/tangle+` |Topological (knot/braid) language; +TangleIR feeds the separate KRL stack + +|007 |`+The-Metadatastician/007+` (private) |Agent meta-language +(anti-scrape; index-only) +|=== + +=== Specialised & DSL + +[width="100%",cols="33%,19%,48%",options="header",] +|=== +|Language |Repo |One-line role +|KitchenSpeak |`+hyperpolymath/kitchenspeak+` |Experimental +kitchen-orchestration DSL +|=== + +=== Exploratory (private; viability under review) + +* *TypeFix Zero (TF0)* — a universe-stratified simply-typed lambda +calculus that separates a total, proof-like fragment from a partial +computational fragment (a single `+fix+` primitive). The repo exists but +is *private*, and its viability is still under review, so it is +index-only here (no public link, as with 007). The design spec is parked +at `+../extraction-queue/typefix-zero/SPEC.adoc+`; it is registered as +`+status = "exploratory"+` in `+../.machine_readable/LANGUAGES.a2ml+`. + +=== Related query/database languages (separate scope) + +These are tracked by the database estate, not this coordinator, and are +listed only for discoverability: + +* *VQL / VQL-DT* — `+hyperpolymath/verisimdb+` (VeriSim Query Language) +* *GQL / GQL-DT* — `+hyperpolymath/lithoglyph+` + +`+hyperpolymath/gql-dt+` +* *FBQL-DT* — `+hyperpolymath/fbql-dt+` (FormDB query language, +dependent types) + +''''' + +____ +Historical note: an earlier version of this file was a pre-pivot +planning snapshot that listed in-tree `+/var/.../REPOS+` paths and hour +estimates. That content is obsolete under the pure-coordinator model and +has been replaced by the pointer above. Planning and status now live in +each language’s own repo and in the canonical trackers listed at the +top. +____ diff --git a/docs/language-portfolio.md b/docs/language-portfolio.md deleted file mode 100644 index 096c8af..0000000 --- a/docs/language-portfolio.md +++ /dev/null @@ -1,68 +0,0 @@ - -# Hyperpolymath Language Portfolio - -**Last updated:** 2026-07-02 - -This is a cross-language index. `nextgen-languages` is a **pure coordinator**: it does not -contain any language. Each language is its own standalone `hyperpolymath/` repo. -**Per-language status, completion, and tech-stack detail are not duplicated here** — they -live in each language's own repo and in the coordinator's canonical trackers: - -- **`.machine_readable/LANGUAGES.a2ml`** — the machine-readable language registry -- **`language-status-tracker.jl`** — the script that computes cross-language status -- **`TOOLING-STATUS.adoc`** — the per-language grade matrix (CRG/TRG/ARG/FRG/RSR) -- **`PROOF-NEEDS.md` / `TEST-NEEDS.md`** — cross-language proof/test gaps - -## General-purpose languages - -| Language | Repo | One-line role | -|----------|------|---------------| -| Phronesis | `hyperpolymath/phronesis` | Formal, auditable agent ethics | -| Eclexia | `hyperpolymath/eclexia` | Resource-first / green computing | -| WokeLang | `hyperpolymath/wokelang` | Consent & well-being as primitives | -| AffineScript | `hyperpolymath/affinescript` | Affine types targeting WasmGC | -| Ephapax | `hyperpolymath/ephapax` | Dyadic linear/affine types → WasmGC | -| My-Lang | `hyperpolymath/my-lang` | Solo → Duet → Ensemble dialect family | -| JtV | `hyperpolymath/jtv` | Systems language, Harvard architecture | -| Error-Lang | `hyperpolymath/error-lang` | Pedagogical, systems thinking via errors | -| Haec | `hyperpolymath/haec` | Trope-particularity: graded property-instance loss, use-checked | -| Oblíbený | `hyperpolymath/oblibeny` | Turing-incomplete secure deployment | -| Anvomidav | `hyperpolymath/anvomidav` | Hard real-time / formal verification | -| betlang | `hyperpolymath/betlang` | Foundational / probabilistic experiment | -| Tangle | `hyperpolymath/tangle` | Topological (knot/braid) language; TangleIR feeds the separate KRL stack | -| 007 | `The-Metadatastician/007` (private) | Agent meta-language (anti-scrape; index-only) | - -## Specialised & DSL - -| Language | Repo | One-line role | -|----------|------|---------------| -| KitchenSpeak | `hyperpolymath/kitchenspeak` | Experimental kitchen-orchestration DSL | - -## Exploratory (private; viability under review) - -- **TypeFix Zero (TF0)** — a universe-stratified simply-typed lambda calculus that separates - a total, proof-like fragment from a partial computational fragment (a single `fix` - primitive). The repo exists but is **private**, and its viability is still under review, so - it is index-only here (no public link, as with 007). The design spec is parked at - `../extraction-queue/typefix-zero/SPEC.adoc`; it is registered as `status = "exploratory"` - in `../.machine_readable/LANGUAGES.a2ml`. - -## Related query/database languages (separate scope) - -These are tracked by the database estate, not this coordinator, and are listed only for -discoverability: - -- **VQL / VQL-DT** — `hyperpolymath/verisimdb` (VeriSim Query Language) -- **GQL / GQL-DT** — `hyperpolymath/lithoglyph` + `hyperpolymath/gql-dt` -- **FBQL-DT** — `hyperpolymath/fbql-dt` (FormDB query language, dependent types) - ---- - -> Historical note: an earlier version of this file was a pre-pivot planning snapshot that -> listed in-tree `/var/.../REPOS` paths and hour estimates. That content is obsolete under -> the pure-coordinator model and has been replaced by the pointer above. Planning and -> status now live in each language's own repo and in the canonical trackers listed at the -> top. diff --git a/docs/reports/audit/audit-2026-04-04.adoc b/docs/reports/audit/audit-2026-04-04.adoc new file mode 100644 index 0000000..b492d73 --- /dev/null +++ b/docs/reports/audit/audit-2026-04-04.adoc @@ -0,0 +1,190 @@ +== Audit Report — nextgen-languages (2026-04-04) + +=== Summary + +Nextgen-languages is a monorepo containing 7+ programming language +projects (tangle, ephapax, wokelang, oblibeny, affinescript, error-lang, +me-dialect, plus infrastructure). The codebase exhibits strong RSR +compliance at the monorepo level with comprehensive CI enforcement. This +audit covers top-level files and subdirectory dangerous pattern +scanning. Individual language projects vary in proof maturity but all +adhere to dangerous pattern policy. + +=== Findings + +==== Critical + +* *RSR compliance at monorepo level*: All top-level artifacts present ✓ +* *Dangerous pattern policy enforced*: Machine-readable policies bind +all subprojects +* *No believe_me detected in top-level files* +* *Individual projects have varying completion* — see subdirectory +verdicts + +==== High + +* *6 Admitted lemmas remain in ephapax* (Rocq 9.1.1, documented in +SESSION-2026-03-28) +* *1 sorry, 2 Admitted in wokelang* (ROADMAP line 12: "`Eliminate +sorry/Admitted (dangerous patterns)`") +* These are documented proof gaps, not hidden defects + +==== Medium + +* Language projects are at varying maturity levels (research through +beta) +* WASM compilation targets for some languages add cross-cutting concerns +* Test infrastructure varies by language (OCaml-heavy, Rust-moderate, +ReScript-light) + +=== RSR Compliance (Monorepo Level) + +* *EXPLAINME.adoc*: present ✓ +* *0-AI-MANIFEST.a2ml*: present ✓ +* *.machine_readable/*: present ✓ +* *SECURITY.md*: present ✓ +* *CONTRIBUTING.md*: present ✓ + +Individual subprojects maintain their own copies where needed: - +ephapax/, wokelang/, error-lang/, betlang/, jtv/, anvomidav/, +phronesis/, tangle/ — All have 0-AI-MANIFEST.a2ml - Most have +SECURITY.md, CONTRIBUTING.md, EXPLAINME.adoc + +=== Test Coverage + +Test coverage varies by subproject language: + +*OCaml (tangle, affinescript)*: - test/ directories with OCamlUnit tests +- tangle/compiler/test/ — test_parser.ml, test_typecheck.ml - +affinescript/test/ — test_golden.ml, test_lexer.ml - affinescript/tests/ +— borrow, codegen, modules, types test suites (70+ test files) + +*Rocq/Coq (ephapax)*: - Formal proofs (20 Qed, 6 Admitted remaining) - +SESSION-2026-03-28 audit documented status - compile clean, no errors + +*Elixir/Gleam (wokelang, phronesis)*: - phronesis/test_stdlib.exs, +test_e2e.exs - phronesis/lib/phronesis/test_framework.ex - +wokelang/ROADMAP specifies test targets + +*Rust (eclexia, tangle backend)*: - +eclexia/compiler/eclexia/src/test_runner.rs - tangle-wasm test +infrastructure + +*JavaScript/TypeScript* (banned language, not in use) - +npm-bun-blocker.yml enforces non-use - ts-blocker.yml enforces non-use + +Overall: Strong test coverage across functional languages, appropriate +for research stage. + +=== Proof Debt + +*Status: MIXED, ACTIVELY MANAGED* + +Dangerous pattern status across monorepo: + +[arabic] +. *believe_me*: 0 active uses detected ✓ +. *assert_total*: 0 uses in primary code (Idris2 components enforce zero +policy) +. *Admitted (Coq/Rocq)*: 6 remaining in ephapax +* ephapax/docs/sessions/SESSION-2026-03-28-type-checker-audit.adoc (line +55) +* "`20 Qed, 6 Admitted, 0 errors`" +* Documented as remaining work (SESSION lines 78-105) +. *sorry (Lean)*: 1 use documented in wokelang +* wokelang/ROADMAP (line 12): "`2 Admitted in Coq, 1 sorry in Lean`" +* ROADMAP (line 7): "`Eliminate sorry/Admitted (dangerous patterns)`" +. *unsafeCoerce (Haskell)*: 0 detected (Haskell not primary) +. *Obj.magic (ReScript)*: 0 detected (ReScript not primary) + +Policy enforcement (monorepo-wide): - .machine_readable/MUST.contractile +— Bans believe_me, assert_total, Admitted, unsafeCoerce, Obj.magic - +.machine_readable/6a2/AGENTIC.a2ml — "`Never use banned language +patterns`" - CI enforcement via rsr-antipattern.yml, boj-build.yml, +quality.yml + +Subproject-specific ADRs: - ephapax/0-AI-MANIFEST.a2ml (line 17) — +Policy declaration - wokelang/0-AI-MANIFEST.a2ml — Policy inheritance - +error-lang/0-AI-MANIFEST.a2ml — Policy inheritance + +=== Publication Safety + +*Monorepo Claim*: "`Next-generation programming languages with formal +verification`" + +*Evidence by subproject*: + +[width="99%",cols="30%,20%,28%,22%",options="header",] +|=== +|Language |Claim |Evidence |Status +|Tangle |Dependent types |Rocq/Coq proofs |Beta, proofs 90%+ + +|Ephapax |Type theory |20 Qed, 6 Admitted (remaining) |Research, +documented + +|Wokelang |Formal semantics |Lean/Coq integration |Research, sorry +documented + +|Oblibeny |Effect system |Rocq proofs |Alpha + +|Affinescript |Linear types |OCaml compiler + tests |Alpha, 70+ tests + +|Error-lang |Error handling |Lean4 extraction |Research + +|Me-dialect |Dialect research |Experimental |Research +|=== + +All claims are transparent about development phase. No inflated +assertions detected. + +=== CI Health + +*Status: COMPREHENSIVE, MONOREPO-WIDE* + +Active workflows (15 files at monorepo level): - boj-build.yml — Build +orchestration - codeql.yml — CodeQL scanning - quality.yml — Code +quality - rsr-antipattern.yml — RSR policy enforcement (believe_me, +Admitted, etc.) - npm-bun-blocker.yml, ts-blocker.yml — Language +enforcement (NO TS/JS) - security-policy.yml, secret-scanner.yml — +Security scanning - scorecard-enforcer.yml, scorecard.yml — OpenSSF +scorecard - workflow-linter.yml — CI integrity - +wellknown-enforcement.yml — Standards compliance - semgrep.yml — Code +pattern analysis - instant-sync.yml — Git mirroring + +*No obvious failures*. rsr-antipattern.yml actively scans for dangerous +patterns. All SHA pins verified. + +=== Verdict + +*PUBLISHABLE NOW (MONOREPO) — Individual projects per subdir* + +The nextgen-languages monorepo itself is publication-ready with +excellent infrastructure: + +[arabic] +. *Central RSR compliance* — All required monorepo artifacts present +. *Policy enforcement* — Dangerous patterns actively banned via CI +. *Transparent completion* — Subprojects document their development +phase +. *Strong safety culture* — Multi-language policy consistently applied +. *Comprehensive CI* — 15 workflows with policy + security scanning + +*Subproject verdicts*: - *tangle*: Beta, ~90% proof complete — +PUBLISHABLE - *ephapax*: Research, 6 Admitted remaining — PUBLISHABLE +(with known gaps documented) - *wokelang*: Research, 1 sorry + 2 +Admitted — AFTER REPAIR (downscope claims) - *affinescript*: Alpha, 70+ +tests — PUBLISHABLE - *oblibeny*: Alpha — PUBLISHABLE + +- *error-lang*: Research — PUBLISHABLE - *me-dialect*: Research — +PUBLISHABLE - *phronesis*, *betlang*, *jtv*, *anvomidav*, *7-tentacles*: +Research stage, all PUBLISHABLE + +The remaining Admitted lemmas (8 total across subprojects) are +*documented as remaining work* in ROADMAP/SESSION files—not hidden +defects. This is appropriate for research-stage formal verification +work. + +''''' + +*Audited by*: M2 estate audit (2026-04-04) *Confidence*: HIGH +*Recommendation*: SHIP AS-IS (monorepo) — Individual subprojects per +README/ROADMAP diff --git a/docs/reports/audit/audit-2026-04-04.md b/docs/reports/audit/audit-2026-04-04.md deleted file mode 100644 index 920f19f..0000000 --- a/docs/reports/audit/audit-2026-04-04.md +++ /dev/null @@ -1,172 +0,0 @@ - -# Audit Report — nextgen-languages (2026-04-04) - -## Summary - -Nextgen-languages is a monorepo containing 7+ programming language projects (tangle, ephapax, wokelang, oblibeny, affinescript, error-lang, me-dialect, plus infrastructure). The codebase exhibits strong RSR compliance at the monorepo level with comprehensive CI enforcement. This audit covers top-level files and subdirectory dangerous pattern scanning. Individual language projects vary in proof maturity but all adhere to dangerous pattern policy. - -## Findings - -### Critical - -- **RSR compliance at monorepo level**: All top-level artifacts present ✓ -- **Dangerous pattern policy enforced**: Machine-readable policies bind all subprojects -- **No believe_me detected in top-level files** -- **Individual projects have varying completion** — see subdirectory verdicts - -### High - -- **6 Admitted lemmas remain in ephapax** (Rocq 9.1.1, documented in SESSION-2026-03-28) -- **1 sorry, 2 Admitted in wokelang** (ROADMAP line 12: "Eliminate sorry/Admitted (dangerous patterns)") -- These are documented proof gaps, not hidden defects - -### Medium - -- Language projects are at varying maturity levels (research through beta) -- WASM compilation targets for some languages add cross-cutting concerns -- Test infrastructure varies by language (OCaml-heavy, Rust-moderate, ReScript-light) - -## RSR Compliance (Monorepo Level) - -- **EXPLAINME.adoc**: present ✓ -- **0-AI-MANIFEST.a2ml**: present ✓ -- **.machine_readable/**: present ✓ -- **SECURITY.md**: present ✓ -- **CONTRIBUTING.md**: present ✓ - -Individual subprojects maintain their own copies where needed: -- ephapax/, wokelang/, error-lang/, betlang/, jtv/, anvomidav/, phronesis/, tangle/ — All have 0-AI-MANIFEST.a2ml -- Most have SECURITY.md, CONTRIBUTING.md, EXPLAINME.adoc - -## Test Coverage - -Test coverage varies by subproject language: - -**OCaml (tangle, affinescript)**: -- test/ directories with OCamlUnit tests -- tangle/compiler/test/ — test_parser.ml, test_typecheck.ml -- affinescript/test/ — test_golden.ml, test_lexer.ml -- affinescript/tests/ — borrow, codegen, modules, types test suites (70+ test files) - -**Rocq/Coq (ephapax)**: -- Formal proofs (20 Qed, 6 Admitted remaining) -- SESSION-2026-03-28 audit documented status -- compile clean, no errors - -**Elixir/Gleam (wokelang, phronesis)**: -- phronesis/test_stdlib.exs, test_e2e.exs -- phronesis/lib/phronesis/test_framework.ex -- wokelang/ROADMAP specifies test targets - -**Rust (eclexia, tangle backend)**: -- eclexia/compiler/eclexia/src/test_runner.rs -- tangle-wasm test infrastructure - -**JavaScript/TypeScript** (banned language, not in use) -- npm-bun-blocker.yml enforces non-use -- ts-blocker.yml enforces non-use - -Overall: Strong test coverage across functional languages, appropriate for research stage. - -## Proof Debt - -**Status: MIXED, ACTIVELY MANAGED** - -Dangerous pattern status across monorepo: - -1. **believe_me**: 0 active uses detected ✓ - -2. **assert_total**: 0 uses in primary code (Idris2 components enforce zero policy) - -3. **Admitted (Coq/Rocq)**: 6 remaining in ephapax - - ephapax/docs/sessions/SESSION-2026-03-28-type-checker-audit.adoc (line 55) - - "20 Qed, 6 Admitted, 0 errors" - - Documented as remaining work (SESSION lines 78-105) - -4. **sorry (Lean)**: 1 use documented in wokelang - - wokelang/ROADMAP (line 12): "2 Admitted in Coq, 1 sorry in Lean" - - ROADMAP (line 7): "Eliminate sorry/Admitted (dangerous patterns)" - -5. **unsafeCoerce (Haskell)**: 0 detected (Haskell not primary) - -6. **Obj.magic (ReScript)**: 0 detected (ReScript not primary) - -Policy enforcement (monorepo-wide): -- .machine_readable/MUST.contractile — Bans believe_me, assert_total, Admitted, unsafeCoerce, Obj.magic -- .machine_readable/6a2/AGENTIC.a2ml — "Never use banned language patterns" -- CI enforcement via rsr-antipattern.yml, boj-build.yml, quality.yml - -Subproject-specific ADRs: -- ephapax/0-AI-MANIFEST.a2ml (line 17) — Policy declaration -- wokelang/0-AI-MANIFEST.a2ml — Policy inheritance -- error-lang/0-AI-MANIFEST.a2ml — Policy inheritance - -## Publication Safety - -**Monorepo Claim**: "Next-generation programming languages with formal verification" - -**Evidence by subproject**: - -| Language | Claim | Evidence | Status | -|----------|-------|----------|--------| -| Tangle | Dependent types | Rocq/Coq proofs | Beta, proofs 90%+ | -| Ephapax | Type theory | 20 Qed, 6 Admitted (remaining) | Research, documented | -| Wokelang | Formal semantics | Lean/Coq integration | Research, sorry documented | -| Oblibeny | Effect system | Rocq proofs | Alpha | -| Affinescript | Linear types | OCaml compiler + tests | Alpha, 70+ tests | -| Error-lang | Error handling | Lean4 extraction | Research | -| Me-dialect | Dialect research | Experimental | Research | - -All claims are transparent about development phase. No inflated assertions detected. - -## CI Health - -**Status: COMPREHENSIVE, MONOREPO-WIDE** - -Active workflows (15 files at monorepo level): -- boj-build.yml — Build orchestration -- codeql.yml — CodeQL scanning -- quality.yml — Code quality -- rsr-antipattern.yml — RSR policy enforcement (believe_me, Admitted, etc.) -- npm-bun-blocker.yml, ts-blocker.yml — Language enforcement (NO TS/JS) -- security-policy.yml, secret-scanner.yml — Security scanning -- scorecard-enforcer.yml, scorecard.yml — OpenSSF scorecard -- workflow-linter.yml — CI integrity -- wellknown-enforcement.yml — Standards compliance -- semgrep.yml — Code pattern analysis -- instant-sync.yml — Git mirroring - -**No obvious failures**. rsr-antipattern.yml actively scans for dangerous patterns. All SHA pins verified. - -## Verdict - -**PUBLISHABLE NOW (MONOREPO) — Individual projects per subdir** - -The nextgen-languages monorepo itself is publication-ready with excellent infrastructure: - -1. **Central RSR compliance** — All required monorepo artifacts present -2. **Policy enforcement** — Dangerous patterns actively banned via CI -3. **Transparent completion** — Subprojects document their development phase -4. **Strong safety culture** — Multi-language policy consistently applied -5. **Comprehensive CI** — 15 workflows with policy + security scanning - -**Subproject verdicts**: -- **tangle**: Beta, ~90% proof complete — PUBLISHABLE -- **ephapax**: Research, 6 Admitted remaining — PUBLISHABLE (with known gaps documented) -- **wokelang**: Research, 1 sorry + 2 Admitted — AFTER REPAIR (downscope claims) -- **affinescript**: Alpha, 70+ tests — PUBLISHABLE -- **oblibeny**: Alpha — PUBLISHABLE -- **error-lang**: Research — PUBLISHABLE -- **me-dialect**: Research — PUBLISHABLE -- **phronesis**, **betlang**, **jtv**, **anvomidav**, **7-tentacles**: Research stage, all PUBLISHABLE - -The remaining Admitted lemmas (8 total across subprojects) are **documented as remaining work** in ROADMAP/SESSION files—not hidden defects. This is appropriate for research-stage formal verification work. - ---- - -**Audited by**: M2 estate audit (2026-04-04) -**Confidence**: HIGH -**Recommendation**: SHIP AS-IS (monorepo) — Individual subprojects per README/ROADMAP diff --git a/docs/tech-debt-2026-05-26.adoc b/docs/tech-debt-2026-05-26.adoc new file mode 100644 index 0000000..7e167b0 --- /dev/null +++ b/docs/tech-debt-2026-05-26.adoc @@ -0,0 +1,84 @@ +== Tech-Debt Audit — nextgen-languages — 2026-05-26 + +*Source:* estate-wide automated scan 2026-05-26. *Companion:* +https://github.com/hyperpolymath/standards/tree/main/docs/audits[`+hyperpolymath/standards+` +2026-05-26-estate-*-debt audits]. *Combined severity:* `+LOW+`. + +This file records the _raw findings_ — it does not by itself fix the +debt. Each section ends with a '`Recommended next move`' line; closing +the debt is follow-up work. + +=== 1. Proof debt + +Scanner counted the following markers in proof-bearing files of this +repo: + +.... +files= 1 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 1 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0 +.... + +*Total markers:* 1. *Severity:* `+>01+`. + +*Marker types* (any non-zero counts above): - Coq `+Axiom+`/`+Admitted+` +— unconditional proof escapes. - Lean `+sorry+`/`+axiom+` — Lean’s +equivalent. - Agda `+postulate+` — accepted axiomatically. - Idris2 +`+believe_me+`/`+assert_total+` — runtime-safe coercion / totality +assumption. - Idris2 top-level `+partial+` — totality-check waived. - F* +`+assume val+`/`+admit_p+` — F* admit. - `+TODO PROOF+` / `+OWED:+` — +self-documented debt markers. - `+unsafePerformIO+`/`+unsafeCoerce+` — +soundness-relevant escape hatches in Haskell/Rust source. + +*Recommended next move:* triage each finding into one of: (a) discharge +by proof, (b) cover with property-tests + a documented refutation +budget, or (c) annotate as a known/necessary axiom (e.g. `+funExt+`) in +`+docs/proof-debt.md+`. + +=== 2. Licence debt + +[cols=",",options="header",] +|=== +|Field |Value +|LICENSE file |`+LICENSE+` +|SPDX header |`+MPL-2.0+` +|Manifest licence |`+NONE+` +|Body classifier |`+Palimp-MPL-2.0+` +|Severity |`+ok+` +|=== + +*Recommended next move:* none for licence. + +=== 3. Documentation debt + +[cols=",",options="header",] +|=== +|Field |Value +|README lines |181 +|`+docs/+` files |10 +|`+docs/+` LoC |2387 +|CHANGELOG.md |Y +|CONTRIBUTING.md |Y +|CODE_OF_CONDUCT.md |Y +|SECURITY.md |Y +|Severity |`+LOW+` +|=== + +*Recommended next move:* `+docs/+` has only 10 file(s). Aim for ≥10 +organised docs (architecture, usage, contributing-guide, +troubleshooting, design-decisions). The user’s bar for a +"`heavily-developed and well-organised wiki`" is ≥10 files with topical +organisation. + +=== Cross-references + +* Estate proof-debt audit: +`+hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md+` +* Estate licence-debt audit: +`+hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md+` +* Estate documentation-debt audit: +`+hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md+` + +''''' + +🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). +This file is informational — closing the debt is follow-up work owned by +the maintainer. diff --git a/docs/tech-debt-2026-05-26.md b/docs/tech-debt-2026-05-26.md deleted file mode 100644 index 8aead31..0000000 --- a/docs/tech-debt-2026-05-26.md +++ /dev/null @@ -1,70 +0,0 @@ - -# Tech-Debt Audit — nextgen-languages — 2026-05-26 - -**Source:** estate-wide automated scan 2026-05-26. -**Companion:** [`hyperpolymath/standards` 2026-05-26-estate-*-debt audits](https://github.com/hyperpolymath/standards/tree/main/docs/audits). -**Combined severity:** `LOW`. - -This file records the *raw findings* — it does not by itself fix the debt. Each section ends with a 'Recommended next move' line; closing the debt is follow-up work. - -## 1. Proof debt - -Scanner counted the following markers in proof-bearing files of this repo: - -``` -files= 1 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 1 | Idr-blv= 0 | Idr-prtl= 0 | Fstr-asm= 0 | TODO= 0 | Unsafe= 0 -``` - -**Total markers:** 1. **Severity:** `>01`. - -**Marker types** (any non-zero counts above): -- Coq `Axiom`/`Admitted` — unconditional proof escapes. -- Lean `sorry`/`axiom` — Lean's equivalent. -- Agda `postulate` — accepted axiomatically. -- Idris2 `believe_me`/`assert_total` — runtime-safe coercion / totality assumption. -- Idris2 top-level `partial` — totality-check waived. -- F\* `assume val`/`admit_p` — F\* admit. -- `TODO PROOF` / `OWED:` — self-documented debt markers. -- `unsafePerformIO`/`unsafeCoerce` — soundness-relevant escape hatches in Haskell/Rust source. - -**Recommended next move:** triage each finding into one of: (a) discharge by proof, (b) cover with property-tests + a documented refutation budget, or (c) annotate as a known/necessary axiom (e.g. `funExt`) in `docs/proof-debt.md`. - -## 2. Licence debt - -| Field | Value | -|---|---| -| LICENSE file | `LICENSE` | -| SPDX header | `MPL-2.0` | -| Manifest licence | `NONE` | -| Body classifier | `Palimp-MPL-2.0` | -| Severity | `ok` | - -**Recommended next move:** none for licence. - -## 3. Documentation debt - -| Field | Value | -|---|---| -| README lines | 181 | -| `docs/` files | 10 | -| `docs/` LoC | 2387 | -| CHANGELOG.md | Y | -| CONTRIBUTING.md | Y | -| CODE_OF_CONDUCT.md | Y | -| SECURITY.md | Y | -| Severity | `LOW` | - -**Recommended next move:** `docs/` has only 10 file(s). Aim for ≥10 organised docs (architecture, usage, contributing-guide, troubleshooting, design-decisions). The user's bar for a "heavily-developed and well-organised wiki" is ≥10 files with topical organisation. - -## Cross-references - -- Estate proof-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-proof-debt.md` -- Estate licence-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-licence-debt.md` -- Estate documentation-debt audit: `hyperpolymath/standards/docs/audits/2026-05-26-estate-documentation-debt.md` - ---- - -🤖 Generated by Claude Code estate-wide tech-debt scan (2026-05-26). This file is informational — closing the debt is follow-up work owned by the maintainer. diff --git a/extraction-queue/affinescript/wiki-AffineScript.md b/extraction-queue/affinescript/wiki-AffineScript.adoc similarity index 83% rename from extraction-queue/affinescript/wiki-AffineScript.md rename to extraction-queue/affinescript/wiki-AffineScript.adoc index c09c624..d244b09 100644 --- a/extraction-queue/affinescript/wiki-AffineScript.md +++ b/extraction-queue/affinescript/wiki-AffineScript.adoc @@ -1,28 +1,29 @@ - -# AffineScript +== AffineScript -**Tagline:** Affine types, dependent types, and effects for WebAssembly +*Tagline:* Affine types, dependent types, and effects for WebAssembly -## Overview +=== Overview -AffineScript combines multiple advanced type system features into a cohesive language targeting WebAssembly: +AffineScript combines multiple advanced type system features into a +cohesive language targeting WebAssembly: -- **Affine Types**: Values can be used at most once -- **Dependent Types**: Types can depend on runtime values -- **Row Polymorphism**: Flexible record and variant handling -- **Effect System**: Explicit side effect tracking -- **WebAssembly**: Broad deployment target +* *Affine Types*: Values can be used at most once +* *Dependent Types*: Types can depend on runtime values +* *Row Polymorphism*: Flexible record and variant handling +* *Effect System*: Explicit side effect tracking +* *WebAssembly*: Broad deployment target -## Philosophy +=== Philosophy -AffineScript explores how advanced type theory can be made practical. By combining affine types (resource safety without GC), dependent types (precise specifications), and effect tracking (purity guarantees), it enables verified software components that run anywhere WebAssembly runs. +AffineScript explores how advanced type theory can be made practical. By +combining affine types (resource safety without GC), dependent types +(precise specifications), and effect tracking (purity guarantees), it +enables verified software components that run anywhere WebAssembly runs. -## Quick Start +=== Quick Start -```ocaml +[source,ocaml] +---- (* Hello World *) let main : Effect[IO] Unit = print "Hello, AffineScript!" @@ -40,15 +41,16 @@ let safe_index : forall (n : Nat). Vector n Int -> Fin n -> Int = (* Row polymorphism for extensible records *) let get_name : forall r. { name : String | r } -> String = fun record -> record.name (* works with any record having 'name' *) -``` +---- -## Type System +=== Type System -### Affine Types +==== Affine Types Variables with affine types can be used at most once: -```ocaml +[source,ocaml] +---- (* Linear: must use exactly once *) type Linear a @@ -66,13 +68,14 @@ let data = File.read handle (* handle consumed here *) (* Explicit drop for affine values *) let unused : Affine Connection = connect server drop unused (* explicit cleanup *) -``` +---- -### Dependent Types +==== Dependent Types Types that depend on values: -```ocaml +[source,ocaml] +---- (* Length-indexed vectors *) type Vector (n : Nat) a @@ -90,13 +93,14 @@ let index : forall n a. Vector n a -> Fin n -> a let vec : Vector 5 Int = [1, 2, 3, 4, 5] let third : Int = index vec 2 (* 2 : Fin 5, statically valid *) (* let sixth = index vec 5 *) (* ERROR: 5 is not < 5 *) -``` +---- -### Row Polymorphism +==== Row Polymorphism Work with records having at least certain fields: -```ocaml +[source,ocaml] +---- (* Function works with any record having 'x' and 'y' *) let distance : forall r. { x : Float, y : Float | r } -> Float = fun point -> sqrt (point.x * point.x + point.y * point.y) @@ -113,13 +117,14 @@ distance named (* works! ignores name *) (* Extending records *) let add_z : forall r. { x : Float, y : Float | r } -> Float -> { x : Float, y : Float, z : Float | r } = fun record z -> { ...record, z = z } -``` +---- -### Effect System +==== Effect System Track and control side effects: -```ocaml +[source,ocaml] +---- (* Effect types *) type Effect e a (* computation with effects 'e' returning 'a' *) @@ -149,13 +154,14 @@ let run_state : forall s a. s -> Effect[State s] a -> (a, s) = handle computation with | get () k -> k init | put s k -> let (r, _) = k () in (r, s) -``` +---- -## Syntax +=== Syntax -### Declarations +==== Declarations -```ocaml +[source,ocaml] +---- (* Value binding *) let name : Type = expr @@ -186,11 +192,12 @@ type Person = { effect MyEffect = | Operation1 : Int -> String | Operation2 : Unit -> Unit -``` +---- -### Expressions +==== Expressions -```ocaml +[source,ocaml] +---- (* Lambda *) fun x -> x + 1 fun (x : Int) (y : Int) -> x + y @@ -221,13 +228,14 @@ perform Operation1 42 handle expr with | Operation1 n k -> k (show n) | Operation2 () k -> k () -``` +---- -## WebAssembly Compilation +=== WebAssembly Compilation AffineScript compiles to efficient WebAssembly: -```ocaml +[source,ocaml] +---- (* Source *) let factorial (n : Nat) : Nat = match n with @@ -242,11 +250,12 @@ let factorial (n : Nat) : Nat = (i64.mul (local.get $n) (call $factorial (i64.sub (local.get $n) (i64.const 1))))))) -``` +---- -### Linear Types → Zero-Cost Resource Management +==== Linear Types → Zero-Cost Resource Management -```ocaml +[source,ocaml] +---- (* Source with linear types *) let with_file (path : String) (f : Linear (Handle File) -> a) : Effect[IO] a = let handle = File.open path in @@ -255,11 +264,12 @@ let with_file (path : String) (f : Linear (Handle File) -> a) : Effect[IO] a = (* Compiles to WASM without GC overhead *) (* Resources are deterministically freed at scope end *) -``` +---- -### WASM Targets +==== WASM Targets -```bash +[source,bash] +---- # Compile to standalone WASM affine build --target wasm32-unknown-unknown src/main.af @@ -268,13 +278,14 @@ affine build --target wasm32-web src/main.af # Compile for WASI (server-side) affine build --target wasm32-wasi src/main.af -``` +---- -## Echidna Integration +=== Echidna Integration -### Type System Soundness +==== Type System Soundness -```agda +[source,agda] +---- -- Prove progress and preservation progress : ∀ {Γ e τ} → Γ ⊢ e : τ → Value e ⊎ ∃[ e' ] (e ⟶ e') preservation : ∀ {Γ e e' τ} → Γ ⊢ e : τ → e ⟶ e' → Γ ⊢ e' : τ @@ -283,11 +294,12 @@ preservation : ∀ {Γ e e' τ} → Γ ⊢ e : τ → e ⟶ e' → Γ ⊢ e' : linearity-sound : ∀ {Γ e τ} → Γ ⊢ e : Linear τ → UsedOnce e -``` +---- -### Property Verification +==== Property Verification -```ocaml +[source,ocaml] +---- (* Specify properties *) @property("vectors preserve length") let concat_length : forall m n a. @@ -300,11 +312,12 @@ let test_concat = let v1 = [1, 2, 3] : Vector 3 Int in let v2 = [4, 5] : Vector 2 Int in assert (length (append v1 v2) = 5) -``` +---- -## Standard Library Highlights +=== Standard Library Highlights -```ocaml +[source,ocaml] +---- (* Linear I/O *) module Linear.IO where type Handle a (* Linear file handle *) @@ -335,11 +348,12 @@ module Control.Effect where val runState : s -> Effect[State s] a -> (a, s) val evalState : s -> Effect[State s] a -> a val execState : s -> Effect[State s] a -> s -``` +---- -## Example: Type-Safe Database +=== Example: Type-Safe Database -```ocaml +[source,ocaml] +---- (* Schema as types *) type Schema = [Column] type Column = { name : String, ty : Type } @@ -367,11 +381,11 @@ let get_user_names : Effect[DB] (List { name : String }) = let add_user : Effect[DB] Unit = insert { id = 1, name = "Alice", email = "alice@example.com" } users_table -``` +---- -## Related Pages +=== Related Pages -- [[Type System Verification]] -- [[WebAssembly Backend]] -- [[Effect System]] -- [[Linear Types]] +* [[Type System Verification]] +* [[WebAssembly Backend]] +* [link:#effect-system[Effect System]] +* [[Linear Types]] diff --git a/extraction-queue/anvomidav/wiki-Anvomidav.adoc b/extraction-queue/anvomidav/wiki-Anvomidav.adoc new file mode 100644 index 0000000..ee8beba --- /dev/null +++ b/extraction-queue/anvomidav/wiki-Anvomidav.adoc @@ -0,0 +1,87 @@ +== Anvomidav + +____ +Maximalist formal verification for hard real-time systems +____ + +*Status:* 📝 Placeholder - contributions welcome + +=== Overview + +Anvomidav combines linear types, session types, and dependent types to +provide maximum formal guarantees for hard real-time systems. Every +resource is tracked, every protocol is verified, every deadline is +statically guaranteed. + +=== Core Invariant + +*Every resource is tracked, every deadline is statically guaranteed.* + +=== Key Features + +* `+task @sched(EDF)+` - Real-time task scheduling +* `+Linear+` - Linear resource tracking +* `+Π (...) . T+` - Dependent type specifications +* Session types for protocol verification + +=== Example + +[source,anvomidav] +---- +// Dependent type: vector of exactly n elements +type Vec(n: Nat, T: Type) = ... + +// Linear type: must be used exactly once +fn open_sensor() -> Linear { ... } + +// Real-time task with deadline +task @sched(EDF) @deadline(10ms) @wcet(5ms) +fn read_sensor(handle: Linear) -> Reading { + let data = handle.read() // handle consumed here + process(data) +} + +// Session type: protocol specification +session SensorProtocol { + !Init. // send init + ?Ack. // receive ack + rec Loop { + !Request. + ?Data. + Loop + } +} +---- + +=== Use Cases + +* Avionics systems (DO-178C compliance) +* Autonomous vehicle control +* Medical device software +* Robotics control systems +* Nuclear and industrial control + +=== Type System + +[cols=",",options="header",] +|=== +|Type Feature |Purpose +|Linear types |Resource safety +|Session types |Protocol correctness +|Dependent types |Value-level specs +|Refinement types |Constraint encoding +|=== + +=== Getting Started + +[source,bash] +---- +cd anvomidav +cargo run +---- + +=== See Also + +* [[NEUROSYM.scm]] - Verification framework +* [[Oblíbený]] - Security guarantees +* [[Testing Framework]] - Echidna integration diff --git a/extraction-queue/anvomidav/wiki-Anvomidav.md b/extraction-queue/anvomidav/wiki-Anvomidav.md deleted file mode 100644 index 210df44..0000000 --- a/extraction-queue/anvomidav/wiki-Anvomidav.md +++ /dev/null @@ -1,82 +0,0 @@ - -# Anvomidav - -> Maximalist formal verification for hard real-time systems - -**Status:** 📝 Placeholder - contributions welcome - -## Overview - -Anvomidav combines linear types, session types, and dependent types to provide maximum formal guarantees for hard real-time systems. Every resource is tracked, every protocol is verified, every deadline is statically guaranteed. - -## Core Invariant - -**Every resource is tracked, every deadline is statically guaranteed.** - -## Key Features - -- `task @sched(EDF)` - Real-time task scheduling -- `Linear` - Linear resource tracking -- `Π (...) . T` - Dependent type specifications -- Session types for protocol verification - -## Example - -```anvomidav -// Dependent type: vector of exactly n elements -type Vec(n: Nat, T: Type) = ... - -// Linear type: must be used exactly once -fn open_sensor() -> Linear { ... } - -// Real-time task with deadline -task @sched(EDF) @deadline(10ms) @wcet(5ms) -fn read_sensor(handle: Linear) -> Reading { - let data = handle.read() // handle consumed here - process(data) -} - -// Session type: protocol specification -session SensorProtocol { - !Init. // send init - ?Ack. // receive ack - rec Loop { - !Request. - ?Data. - Loop - } -} -``` - -## Use Cases - -- Avionics systems (DO-178C compliance) -- Autonomous vehicle control -- Medical device software -- Robotics control systems -- Nuclear and industrial control - -## Type System - -| Type Feature | Purpose | -|--------------|---------| -| Linear types | Resource safety | -| Session types | Protocol correctness | -| Dependent types | Value-level specs | -| Refinement types | Constraint encoding | - -## Getting Started - -```bash -cd anvomidav -cargo run -``` - -## See Also - -- [[NEUROSYM.scm]] - Verification framework -- [[Oblíbený]] - Security guarantees -- [[Testing Framework]] - Echidna integration diff --git a/extraction-queue/betlang/wiki-betlang.adoc b/extraction-queue/betlang/wiki-betlang.adoc new file mode 100644 index 0000000..e11e52d --- /dev/null +++ b/extraction-queue/betlang/wiki-betlang.adoc @@ -0,0 +1,86 @@ +== betlang + +*Tagline:* A symbolic probabilistic metalanguage — a _probabilistic +computer algebra system_, not a betting language. + +=== Overview + +BetLang is built on one idea: *computation is structured choice under +uncertainty.* Its core primitive is the ternary form `+(bet A B C)+` — a +probabilistic, *lazy* choice between three branches (only the selected +branch is evaluated). This makes BetLang closer to a _probabilistic CAS_ +than a simulation DSL: it is symbolic-first, compositional, and treats +uncertainty as a first-class *typed* object rather than as noise to +average away. + +=== Philosophy + +* *Ternary over binary* — real-world decisions are rarely yes/no; the +musical ternary form (A–B–A) gives compositional structure, and +Dutch-book coherence needs ≥3 outcomes. +* *Uncertainty as structure* — not noise, but a first-class object the +type system tracks. +* *Symbolic first* — computation stays inspectable and composable. + +=== Core Primitive + +[source,racket] +---- +#lang betlang + +(bet 'win 'draw 'lose) ; uniform ternary choice (lazy) +(bet/weighted '(common 7) '(uncommon 2) '(rare 1)) ; non-uniform +(bet/conditional pred A B C) ; predicate-driven +(bet (expensive) (cheap-approx) (fallback)) ; only one branch is evaluated +---- + +=== Type System + +BetLang’s checker (`+bet-check+`, Rust) is Hindley–Milner with two +domain-specific pillars: + +* *Echo types* — _structured loss_ as a typed object. When a `+bet+` +collapses three branches to one (or a `+sample+` marginalises a draw), +`+Echo T+` retains a proof-relevant residue of what was lost; `+Echo T+` +is deliberately *distinct from `+T+`* (no implicit forgetting). The +operations form a functor + comonad surface (`+echo+`, `+echo_output+`, +`+echo_map+`, `+echo_duplicate+`, `+echo_to_residue+`, `+sample_echo+`), +the ungraded ghost shadow of the graded comonad proved in +https://github.com/hyperpolymath/echo-types[`+echo-types+`] (Agda). +* *The uncertainty number tower* — 14 uncertainty-aware number systems +(Gaussian, interval/affine, fuzzy, Bayesian, VaR/CVaR, surreal, p-adic, +imprecise, Dempster–Shafer, …). These _are_ the type system, not +add-ons. + +=== Formal Verification + +The core calculus is mechanised in *Lean 4* (`+proofs/BetLang.lean+`, +CI-checked): *Progress*, *Preservation*, and the *distribution monad +laws* — with an *axiom-free core* (the `+substTop_preserves_typing+` +axiom was discharged) and *zero `+sorry+`*. This is BetLang’s +differentiator versus untyped numeric/CAS tools (R, Octave, Scilab, +Mathematica, Maple): _typed, proof-anchored uncertainty_. + +=== Architecture + +Four layers with separated responsibilities: *Racket* (authoritative +semantics) · *Julia* (compute kernel / number tower) · *Lean 4* (proofs) +· *Rust* (compiler tooling — `+bet-core+`, `+bet-check+`, +`+bet-parse+`). + +=== Status + +Active. Racket frontend authoritative; Lean proofs machine-checked +(axiom-free core); Rust checker handles Echo formers *and* the typed +echo operations; Julia backend in active development. + +=== See Also + +* BetLang repository wiki (in-repo `+wiki/+`): Home · Type-System · +Echo-Types · Formal-Verification · Number-Tower +* [[Ephapax]] — linear/affine once-only semantics (sibling language) +* [[AffineScript]] — affine-typed primary application language +* Upstream: https://github.com/hyperpolymath/echo-types[`+echo-types+`] +(Agda, source of truth) · +https://github.com/hyperpolymath/EchoTypes.jl[`+EchoTypes.jl+`] +(executable shadow) diff --git a/extraction-queue/betlang/wiki-betlang.md b/extraction-queue/betlang/wiki-betlang.md deleted file mode 100644 index 33a107a..0000000 --- a/extraction-queue/betlang/wiki-betlang.md +++ /dev/null @@ -1,74 +0,0 @@ - -# betlang - -**Tagline:** A symbolic probabilistic metalanguage — a *probabilistic computer algebra system*, not a betting language. - -## Overview - -BetLang is built on one idea: **computation is structured choice under uncertainty.** -Its core primitive is the ternary form `(bet A B C)` — a probabilistic, **lazy** choice -between three branches (only the selected branch is evaluated). This makes BetLang closer -to a *probabilistic CAS* than a simulation DSL: it is symbolic-first, compositional, and -treats uncertainty as a first-class **typed** object rather than as noise to average away. - -## Philosophy - -- **Ternary over binary** — real-world decisions are rarely yes/no; the musical ternary - form (A–B–A) gives compositional structure, and Dutch-book coherence needs ≥3 outcomes. -- **Uncertainty as structure** — not noise, but a first-class object the type system tracks. -- **Symbolic first** — computation stays inspectable and composable. - -## Core Primitive - -```racket -#lang betlang - -(bet 'win 'draw 'lose) ; uniform ternary choice (lazy) -(bet/weighted '(common 7) '(uncommon 2) '(rare 1)) ; non-uniform -(bet/conditional pred A B C) ; predicate-driven -(bet (expensive) (cheap-approx) (fallback)) ; only one branch is evaluated -``` - -## Type System - -BetLang's checker (`bet-check`, Rust) is Hindley–Milner with two domain-specific pillars: - -- **Echo types** — *structured loss* as a typed object. When a `bet` collapses three - branches to one (or a `sample` marginalises a draw), `Echo T` retains a proof-relevant - residue of what was lost; `Echo T` is deliberately **distinct from `T`** (no implicit - forgetting). The operations form a functor + comonad surface (`echo`, `echo_output`, - `echo_map`, `echo_duplicate`, `echo_to_residue`, `sample_echo`), the ungraded ghost - shadow of the graded comonad proved in [`echo-types`](https://github.com/hyperpolymath/echo-types) (Agda). -- **The uncertainty number tower** — 14 uncertainty-aware number systems (Gaussian, - interval/affine, fuzzy, Bayesian, VaR/CVaR, surreal, p-adic, imprecise, Dempster–Shafer, - …). These *are* the type system, not add-ons. - -## Formal Verification - -The core calculus is mechanised in **Lean 4** (`proofs/BetLang.lean`, CI-checked): -**Progress**, **Preservation**, and the **distribution monad laws** — with an -**axiom-free core** (the `substTop_preserves_typing` axiom was discharged) and **zero -`sorry`**. This is BetLang's differentiator versus untyped numeric/CAS tools (R, Octave, -Scilab, Mathematica, Maple): *typed, proof-anchored uncertainty*. - -## Architecture - -Four layers with separated responsibilities: **Racket** (authoritative semantics) · -**Julia** (compute kernel / number tower) · **Lean 4** (proofs) · **Rust** (compiler -tooling — `bet-core`, `bet-check`, `bet-parse`). - -## Status - -Active. Racket frontend authoritative; Lean proofs machine-checked (axiom-free core); -Rust checker handles Echo formers **and** the typed echo operations; Julia backend in -active development. - -## See Also - -- BetLang repository wiki (in-repo `wiki/`): Home · Type-System · Echo-Types · Formal-Verification · Number-Tower -- [[Ephapax]] — linear/affine once-only semantics (sibling language) -- [[AffineScript]] — affine-typed primary application language -- Upstream: [`echo-types`](https://github.com/hyperpolymath/echo-types) (Agda, source of truth) · [`EchoTypes.jl`](https://github.com/hyperpolymath/EchoTypes.jl) (executable shadow) diff --git a/extraction-queue/eclexia/design/next-steps.adoc b/extraction-queue/eclexia/design/next-steps.adoc new file mode 100644 index 0000000..044dd86 --- /dev/null +++ b/extraction-queue/eclexia/design/next-steps.adoc @@ -0,0 +1,146 @@ +== Eclexia Next Steps: Stdlib Implementation + +*Date:* 2026-02-07 *Current Status:* 90% → 95% (after parser +improvements) + +=== Current State + +==== ✅ Parser (95% Complete) + +* All major syntax features implemented +* 28/32 conformance tests now *parse successfully* (87.5%) +* Remaining 4 parse failures are edge cases + +==== ⚠️ Standard Library (60% Complete) + +*Missing critical components causing test failures:* + +[arabic] +. *`+assert()+` function* (7 test failures) +* Trivial: ~30 minutes +* Just needs panic on false condition +. *`+Option+` type* (3 test failures) +* `+Some(value)+` constructor +* `+None+` value +* Pattern matching support +* Effort: ~2 hours +. *`+Result+` type* (2 test failures) +* `+Ok(value)+` constructor +* `+Err(error)+` constructor +* Pattern matching support +* Effort: ~2 hours +. *`+shadow_price()+` function* (1 test failure) +* Economics-specific runtime query +* Needs resource tracking integration +* Effort: ~3 hours + +==== Total Effort: ~8 hours + +''''' + +=== After Stdlib Implementation + +==== Projected Conformance Test Results + +* *Current:* 5/32 passing (15.6%) +* *Parser fixed:* 28/32 parsing (87.5%) +* *After stdlib:* 28-30/32 passing (87-94%) + +==== Eclexia Completion Percentage + +* *Current:* 90% +* *After parser improvements:* 95% +* *After stdlib implementation:* *98-99%* + +Remaining 1-2% would be: - Edge case bug fixes - Performance +optimizations - VSCode extension packaging - Documentation polish + +''''' + +=== Impact on Overall NextGen Languages Portfolio + +==== Current Verified Status + +[cols=",,",options="header",] +|=== +|Language |Current % |Production Ready? +|*WokeLang* |100% |✅ Yes +|*Eclexia* |95% |⚠️ Almost (missing stdlib) +|*My-Lang* |75%? |❓ Unknown (build blocked) +|=== + +==== After Eclexia Stdlib Implementation + +[cols=",,",options="header",] +|=== +|Language |Projected % |Production Ready? +|*WokeLang* |100% |✅ Yes +|*Eclexia* |*98-99%* |✅ *Yes* +|*My-Lang* |75%? |❓ Unknown (build blocked) +|=== + +''''' + +=== Portfolio Status Summary + +==== If Eclexia Stdlib is Completed: + +* *2 out of 3 languages production-ready* (66% complete) +* *Average completion:* (100% + 99% + 75%) / 3 = *91.3%* +* *Verified average:* (100% + 99%) / 2 = *99.5%* (My-Lang excluded until +verified) + +==== Current State (No Stdlib Work): + +* *1 out of 3 languages production-ready* (33% complete) +* *Average completion:* (100% + 95% + 75%) / 3 = *90%* +* *Verified average:* (100% + 95%) / 2 = *97.5%* + +''''' + +=== Recommendation + +==== Priority: *HIGH* 🔥 + +*Implementing Eclexia’s missing stdlib (8 hours) would:* 1. Complete 2 +out of 3 languages to production-ready state 2. Push portfolio average +to 91%+ 3. Make Eclexia’s economics-as-code paradigm fully usable 4. +Validate dimensional analysis for real-world use cases + +==== Implementation Order: + +[arabic] +. *`+assert()+` function* (30 min) → Quick wins, 7 tests pass +. *`+Option+` type* (2 hours) → Unlocks 3 more tests +. *`+Result+` type* (2 hours) → Unlocks 2 more tests +. *`+shadow_price()+` function* (3 hours) → Economics feature complete + +==== Estimated Timeline: + +* *Single focused session:* 8-10 hours (1 day) +* *Spread over multiple sessions:* 2-3 days + +''''' + +=== My-Lang Status Note + +*Before declaring portfolio complete:* - Install `+openssl-devel+`: +`+sudo dnf install openssl-devel+` - Build My-Lang: +`+cargo build --release+` - Verify actual completion percentage - Update +status documents with real numbers + +If My-Lang is actually at 75%, the missing stdlib work on Eclexia +becomes *even more critical* to maintain a high portfolio completion +rate. + +''''' + +*Bottom Line:* - *Current portfolio:* 90% complete (verified) - *After 8 +hours Eclexia stdlib work:* *91-99% complete* (depending on My-Lang +verification) - *ROI:* Extremely high - 8 hours → production-ready +economics language + +''''' + +*Maintainer:* Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk *Date:* +2026-02-07 *License:* MPL-2.0 diff --git a/extraction-queue/eclexia/design/next-steps.md b/extraction-queue/eclexia/design/next-steps.md deleted file mode 100644 index 9c9745e..0000000 --- a/extraction-queue/eclexia/design/next-steps.md +++ /dev/null @@ -1,141 +0,0 @@ - -# Eclexia Next Steps: Stdlib Implementation -**Date:** 2026-02-07 -**Current Status:** 90% → 95% (after parser improvements) - -## Current State - -### ✅ Parser (95% Complete) -- All major syntax features implemented -- 28/32 conformance tests now **parse successfully** (87.5%) -- Remaining 4 parse failures are edge cases - -### ⚠️ Standard Library (60% Complete) -**Missing critical components causing test failures:** - -1. **`assert()` function** (7 test failures) - - Trivial: ~30 minutes - - Just needs panic on false condition - -2. **`Option` type** (3 test failures) - - `Some(value)` constructor - - `None` value - - Pattern matching support - - Effort: ~2 hours - -3. **`Result` type** (2 test failures) - - `Ok(value)` constructor - - `Err(error)` constructor - - Pattern matching support - - Effort: ~2 hours - -4. **`shadow_price()` function** (1 test failure) - - Economics-specific runtime query - - Needs resource tracking integration - - Effort: ~3 hours - -### Total Effort: ~8 hours - ---- - -## After Stdlib Implementation - -### Projected Conformance Test Results -- **Current:** 5/32 passing (15.6%) -- **Parser fixed:** 28/32 parsing (87.5%) -- **After stdlib:** 28-30/32 passing (87-94%) - -### Eclexia Completion Percentage -- **Current:** 90% -- **After parser improvements:** 95% -- **After stdlib implementation:** **98-99%** - -Remaining 1-2% would be: -- Edge case bug fixes -- Performance optimizations -- VSCode extension packaging -- Documentation polish - ---- - -## Impact on Overall NextGen Languages Portfolio - -### Current Verified Status - -| Language | Current % | Production Ready? | -|----------|-----------|-------------------| -| **WokeLang** | 100% | ✅ Yes | -| **Eclexia** | 95% | ⚠️ Almost (missing stdlib) | -| **My-Lang** | 75%? | ❓ Unknown (build blocked) | - -### After Eclexia Stdlib Implementation - -| Language | Projected % | Production Ready? | -|----------|-------------|-------------------| -| **WokeLang** | 100% | ✅ Yes | -| **Eclexia** | **98-99%** | ✅ **Yes** | -| **My-Lang** | 75%? | ❓ Unknown (build blocked) | - ---- - -## Portfolio Status Summary - -### If Eclexia Stdlib is Completed: -- **2 out of 3 languages production-ready** (66% complete) -- **Average completion:** (100% + 99% + 75%) / 3 = **91.3%** -- **Verified average:** (100% + 99%) / 2 = **99.5%** (My-Lang excluded until verified) - -### Current State (No Stdlib Work): -- **1 out of 3 languages production-ready** (33% complete) -- **Average completion:** (100% + 95% + 75%) / 3 = **90%** -- **Verified average:** (100% + 95%) / 2 = **97.5%** - ---- - -## Recommendation - -### Priority: **HIGH** 🔥 - -**Implementing Eclexia's missing stdlib (8 hours) would:** -1. Complete 2 out of 3 languages to production-ready state -2. Push portfolio average to 91%+ -3. Make Eclexia's economics-as-code paradigm fully usable -4. Validate dimensional analysis for real-world use cases - -### Implementation Order: -1. **`assert()` function** (30 min) → Quick wins, 7 tests pass -2. **`Option` type** (2 hours) → Unlocks 3 more tests -3. **`Result` type** (2 hours) → Unlocks 2 more tests -4. **`shadow_price()` function** (3 hours) → Economics feature complete - -### Estimated Timeline: -- **Single focused session:** 8-10 hours (1 day) -- **Spread over multiple sessions:** 2-3 days - ---- - -## My-Lang Status Note - -**Before declaring portfolio complete:** -- Install `openssl-devel`: `sudo dnf install openssl-devel` -- Build My-Lang: `cargo build --release` -- Verify actual completion percentage -- Update status documents with real numbers - -If My-Lang is actually at 75%, the missing stdlib work on Eclexia becomes **even more critical** to maintain a high portfolio completion rate. - ---- - -**Bottom Line:** -- **Current portfolio:** 90% complete (verified) -- **After 8 hours Eclexia stdlib work:** **91-99% complete** (depending on My-Lang verification) -- **ROI:** Extremely high - 8 hours → production-ready economics language - ---- - -**Maintainer:** Jonathan D.A. Jewell -**Date:** 2026-02-07 -**License:** MPL-2.0 diff --git a/extraction-queue/eclexia/wiki-Eclexia.adoc b/extraction-queue/eclexia/wiki-Eclexia.adoc new file mode 100644 index 0000000..3ee801e --- /dev/null +++ b/extraction-queue/eclexia/wiki-Eclexia.adoc @@ -0,0 +1,74 @@ +== Eclexia + +____ +Sustainable Software Engineering through resource-first constraints +____ + +*Status:* 📝 Placeholder - contributions welcome + +*Note:* Priority sync from GitLab required - 70-page white paper exists +there. + +=== Overview + +Eclexia makes resource consumption a first-class concern in software +design. Energy budgets, memory limits, and computational constraints are +expressed declaratively. + +=== Core Invariant + +*No computation proceeds without an explicit resource budget.* + +=== Key Features + +* `+(energy budget ...)+` - Energy consumption constraints +* `+(resource ...)+` - Resource requirement specification +* Compile-time resource analysis +* Carbon-aware scheduling + +=== Example + +[source,eclexia] +---- +(program sensor-aggregation + (energy budget 100mJ per-invocation) + (resource memory 64KB) + (resource cpu-cycles 10000) + + (define (aggregate readings) + (resource memory 1KB) + (fold + 0 readings)) + + (define (transmit data) + (energy budget 50mJ) + (radio-send data))) + +;; Compiler rejects if budget exceeded +---- + +=== Use Cases + +* Green computing / sustainable software +* IoT and embedded systems +* Cloud cost optimization (FinOps) +* Battery-constrained devices +* Carbon-aware computing + +=== Getting Started + +[source,bash] +---- +cd eclexia +cargo run +---- + +=== Related Work + +* Green Software Foundation principles +* Carbon-aware SDK +* Energy-proportional computing research + +=== See Also + +* [[Oblíbený]] - Security constraints (complementary) +* [[Anvomidav]] - Timing constraints (complementary) diff --git a/extraction-queue/eclexia/wiki-Eclexia.md b/extraction-queue/eclexia/wiki-Eclexia.md deleted file mode 100644 index 44bda1e..0000000 --- a/extraction-queue/eclexia/wiki-Eclexia.md +++ /dev/null @@ -1,71 +0,0 @@ - -# Eclexia - -> Sustainable Software Engineering through resource-first constraints - -**Status:** 📝 Placeholder - contributions welcome - -**Note:** Priority sync from GitLab required - 70-page white paper exists there. - -## Overview - -Eclexia makes resource consumption a first-class concern in software design. Energy budgets, memory limits, and computational constraints are expressed declaratively. - -## Core Invariant - -**No computation proceeds without an explicit resource budget.** - -## Key Features - -- `(energy budget ...)` - Energy consumption constraints -- `(resource ...)` - Resource requirement specification -- Compile-time resource analysis -- Carbon-aware scheduling - -## Example - -```eclexia -(program sensor-aggregation - (energy budget 100mJ per-invocation) - (resource memory 64KB) - (resource cpu-cycles 10000) - - (define (aggregate readings) - (resource memory 1KB) - (fold + 0 readings)) - - (define (transmit data) - (energy budget 50mJ) - (radio-send data))) - -;; Compiler rejects if budget exceeded -``` - -## Use Cases - -- Green computing / sustainable software -- IoT and embedded systems -- Cloud cost optimization (FinOps) -- Battery-constrained devices -- Carbon-aware computing - -## Getting Started - -```bash -cd eclexia -cargo run -``` - -## Related Work - -- Green Software Foundation principles -- Carbon-aware SDK -- Energy-proportional computing research - -## See Also - -- [[Oblíbený]] - Security constraints (complementary) -- [[Anvomidav]] - Timing constraints (complementary) diff --git a/extraction-queue/ephapax/design/dyadic-architecture.md b/extraction-queue/ephapax/design/dyadic-architecture.adoc similarity index 67% rename from extraction-queue/ephapax/design/dyadic-architecture.md rename to extraction-queue/ephapax/design/dyadic-architecture.adoc index da93835..69f5298 100644 --- a/extraction-queue/ephapax/design/dyadic-architecture.md +++ b/extraction-queue/ephapax/design/dyadic-architecture.adoc @@ -1,41 +1,37 @@ - -# Ephapax: Dyadic Language Architecture +== Ephapax: Dyadic Language Architecture -**Date:** 2026-02-07 -**Status:** Architectural clarification +*Date:* 2026-02-07 *Status:* Architectural clarification ---- +''''' -## Critical Understanding +=== Critical Understanding -**Ephapax is NOT a single language.** +*Ephapax is NOT a single language.* -**Ephapax is TWO sister languages** working together in a dyadic relationship: -1. **Ephapax-Linear** - Linear type system language -2. **Ephapax-Affine** - Affine type system language +*Ephapax is TWO sister languages* working together in a dyadic +relationship: 1. *Ephapax-Linear* - Linear type system language 2. +*Ephapax-Affine* - Affine type system language -They share common infrastructure but have distinct type systems and semantics. +They share common infrastructure but have distinct type systems and +semantics. ---- +''''' -## Dyadic Design Principles +=== Dyadic Design Principles -### What "Dyadic" Means +==== What "`Dyadic`" Means -- **Two languages, one repository** -- **Common core** shared by both -- **Language-specific features** for each -- **Unified tooling** with modes for each language -- **Interoperability** between the two languages +* *Two languages, one repository* +* *Common core* shared by both +* *Language-specific features* for each +* *Unified tooling* with modes for each language +* *Interoperability* between the two languages ---- +''''' -## Proposed Repository Structure +=== Proposed Repository Structure -``` +.... ephapax/ ├── common/ # SHARED infrastructure │ ├── lexer/ # Common lexer (both share syntax base) @@ -97,34 +93,38 @@ ephapax/ ├── affine-guide.md # Affine language guide ├── dyadic-programming.md # How to use both together └── type-system-comparison.md -``` +.... ---- +''''' -## File Extension Strategy +=== File Extension Strategy -**Option 1: Single extension with mode markers** -``` +*Option 1: Single extension with mode markers* + +.... program.eph # Default (Linear) #!ephapax-linear # Linear mode marker #!ephapax-affine # Affine mode marker -``` +.... + +*Option 2: Distinct extensions* -**Option 2: Distinct extensions** -``` +.... program.ephl # Ephapax Linear program.epha # Ephapax Affine program.eph # Mixed (both) -``` +.... -**Recommendation:** Use Option 2 for clarity +*Recommendation:* Use Option 2 for clarity ---- +''''' -## Debugger Architecture +=== Debugger Architecture -### Common Debugger Core -```rust +==== Common Debugger Core + +[source,rust] +---- pub struct EphapaxDebugger { common: CommonDebugState, mode: LanguageMode, @@ -135,32 +135,27 @@ pub enum LanguageMode { Affine(AffineDebugger), Mixed(MixedDebugger), } -``` +---- -### Mode-Specific Features +==== Mode-Specific Features -**Linear Mode:** -- Track linear resources (must be used exactly once) -- Show linearity violations -- Inspect consumption points -- Verify no duplication or dropping +*Linear Mode:* - Track linear resources (must be used exactly once) - +Show linearity violations - Inspect consumption points - Verify no +duplication or dropping -**Affine Mode:** -- Track affine resources (used at most once) -- Show borrowing relationships -- Inspect drop points -- Verify no duplication (dropping allowed) +*Affine Mode:* - Track affine resources (used at most once) - Show +borrowing relationships - Inspect drop points - Verify no duplication +(dropping allowed) -**Mixed Mode:** -- Switch between modes -- Show interop boundaries -- Track conversions between Linear ↔ Affine +*Mixed Mode:* - Switch between modes - Show interop boundaries - Track +conversions between Linear ↔ Affine ---- +''''' -## Compiler CLI Interface +=== Compiler CLI Interface -```bash +[source,bash] +---- # Compile Linear program ephapax compile --lang=linear program.ephl -o output @@ -181,13 +176,14 @@ ephapax debug --lang=linear program.ephl # Debugger with Affine mode ephapax debug --lang=affine program.epha -``` +---- ---- +''''' -## State.scm Structure for Ephapax +=== State.scm Structure for Ephapax -```scheme +[source,scheme] +---- (state (metadata (project "ephapax") @@ -240,56 +236,67 @@ ephapax debug --lang=affine program.epha (interop-bridge-minimal (impact "Cannot mix Linear and Affine code effectively") (description "Bridge between languages at 30%"))))) -``` +---- + +''''' + +=== Development Priorities + +==== Phase 1: Complete Common Infrastructure (5-10 hours) + +* Finish shared IR (60% → 100%) +* Complete common runtime (50% → 100%) + +==== Phase 2: Complete Typecheckers (15-20 hours) ---- +* Linear typechecker (60% → 100%) +* Affine typechecker (60% → 100%) -## Development Priorities +==== Phase 3: Unify Debugger (10-15 hours) -### Phase 1: Complete Common Infrastructure (5-10 hours) -- Finish shared IR (60% → 100%) -- Complete common runtime (50% → 100%) +* Linear mode (35% → 100%) +* Affine mode (35% → 100%) +* Mode switching -### Phase 2: Complete Typecheckers (15-20 hours) -- Linear typechecker (60% → 100%) -- Affine typechecker (60% → 100%) +==== Phase 4: Interoperability (10-15 hours) -### Phase 3: Unify Debugger (10-15 hours) -- Linear mode (35% → 100%) -- Affine mode (35% → 100%) -- Mode switching +* Bridge (30% → 100%) +* FFI implementation +* Mixed program examples -### Phase 4: Interoperability (10-15 hours) -- Bridge (30% → 100%) -- FFI implementation -- Mixed program examples +==== Phase 5: Tooling (15-20 hours) -### Phase 5: Tooling (15-20 hours) -- LSP with dual language support -- Formatter -- Linter +* LSP with dual language support +* Formatter +* Linter -**Total to 100%:** ~55-80 hours +*Total to 100%:* ~55-80 hours ---- +''''' -## Critical Insights +=== Critical Insights -1. **Not dialects** - These are sister languages, not variants of one language -2. **Dyadic = Two working together** - They complement each other -3. **Common ≠ Identical** - Share infrastructure but distinct type systems -4. **Unified tooling** - One debugger with two modes, not two debuggers -5. **Interop is critical** - Must be able to use both in same program +[arabic] +. *Not dialects* - These are sister languages, not variants of one +language +. *Dyadic = Two working together* - They complement each other +. *Common ≠ Identical* - Share infrastructure but distinct type systems +. *Unified tooling* - One debugger with two modes, not two debuggers +. *Interop is critical* - Must be able to use both in same program ---- +''''' -## Questions for User +=== Questions for User -1. Should we rename ephapax to reflect dyadic nature? (e.g., "ephapax-dyad")? -2. File extensions: Prefer .ephl/.epha or .eph with markers? -3. Should Linear and Affine be callable from each other (interop), or separate runtimes? -4. Priority: Complete typecheckers first, or build interop bridge? +[arabic] +. Should we rename ephapax to reflect dyadic nature? (e.g., +"`ephapax-dyad`")? +. File extensions: Prefer .ephl/.epha or .eph with markers? +. Should Linear and Affine be callable from each other (interop), or +separate runtimes? +. Priority: Complete typecheckers first, or build interop bridge? ---- +''''' -**This document clarifies Ephapax's unique dyadic architecture for AI agents.** +*This document clarifies Ephapax’s unique dyadic architecture for AI +agents.* diff --git a/extraction-queue/ephapax/design/proven-integration.adoc b/extraction-queue/ephapax/design/proven-integration.adoc new file mode 100644 index 0000000..ed4b21a --- /dev/null +++ b/extraction-queue/ephapax/design/proven-integration.adoc @@ -0,0 +1,138 @@ +== Proven Library Integration Plan + +This document outlines how the +https://github.com/hyperpolymath/proven[proven] library’s formally +verified modules integrate with the Next-Gen Languages ecosystem. + +*Note:* Several Next-Gen Languages (especially Anvomidav and Duet) have +formal verification as core features. The proven library provides shared +verification infrastructure. + +=== Per-Language Integration + +==== Anvomidav (Formal Verification Focus) + +[cols=",,",options="header",] +|=== +|Module |Use Case |Formal Guarantee +|`+SafeThm+` |Theorem statement management |Well-typed propositions +|`+SafeLinear+` |Linear type enforcement |Resource linearity +|`+SafeSession+` |Session type checking |Protocol conformance +|`+SafeRealTime+` |WCET analysis |Bounded execution time +|=== + +Anvomidav’s type system directly corresponds to proven modules: - +`+Linear+` → SafeLinear - `+Session+` → SafeSession - +`+@sched(EDF)+` → SafeRealTime + +==== Duet (AI-Assisted Verification) + +[cols=",,",options="header",] +|=== +|Module |Use Case |Formal Guarantee +|`+SafeProperty+` |Property synthesis targets |Valid specifications +|`+SafeThm+` |AI-generated proof validation |Proof soundness +|`+SafeOracle+` |AI verification oracle |Trusted computation +|=== + +Duet’s `+@verify+` and `+@synth+` annotations use proven as the +verification backend. + +==== Phronesis (AI Ethics/Alignment) + +[width="100%",cols="23%,27%,50%",options="header",] +|=== +|Module |Use Case |Formal Guarantee +|`+SafePolicy+` |Ethical policy specification |Policy consistency +|`+SafeConstraint+` |Value constraint checking |Constraint satisfaction +|`+SafeProvenance+` |Decision audit trails |Accountability +|=== + +Phronesis agents use SafePolicy for ethical framework specification. + +==== Oblíbený (Secure Code) + +[width="100%",cols="23%,27%,50%",options="header",] +|=== +|Module |Use Case |Formal Guarantee +|`+SafeBounded+` |Turing-incomplete enforcement |Termination guarantee +|`+SafeFlow+` |Information flow control |No data leakage +|`+SafeCrypto+` |Cryptographic operations |Correct algorithm usage +|=== + +Oblíbený’s `+(forbid recursion)+` maps to SafeBounded’s termination +proofs. + +==== Eclexia (Resource-Constrained) + +[cols=",,",options="header",] +|=== +|Module |Use Case |Formal Guarantee +|`+SafeResource+` |Resource budget tracking |Budget compliance +|`+SafeEnergy+` |Energy consumption proofs |Bounded energy use +|`+SafeMetric+` |Resource metric validation |Valid measurements +|=== + +Eclexia’s `+(energy budget ...)+` uses SafeEnergy for compile-time +verification. + +==== Solo (Foundation Language) + +[cols=",,",options="header",] +|=== +|Module |Use Case |Formal Guarantee +|`+SafeContract+` |Pre/post conditions |Contract satisfaction +|`+SafeConcurrent+` |Concurrency safety |Race-freedom +|`+SafeEffect+` |Effect tracking |Effect containment +|=== + +Solo’s `+where { pre: ..., post: ... }+` uses SafeContract. + +==== Ensemble (AI-Native) + +[cols=",,",options="header",] +|=== +|Module |Use Case |Formal Guarantee +|`+SafeOracle+` |AI model invocation |Trusted AI calls +|`+SafeEffect+` |AI effect isolation |Effect boundaries +|`+SafeSchema+` |Prompt validation |Well-formed prompts +|=== + +==== WokeLang (Human-Centric) + +[cols=",,",options="header",] +|=== +|Module |Use Case |Formal Guarantee +|`+SafeConsent+` |Consent tracking |Explicit consent +|`+SafePrivacy+` |Privacy enforcement |Data protection +|`+SafeAccessibility+` |A11y compliance |Accessibility checks +|=== + +=== Shared Infrastructure + +All Next-Gen Languages share these proven modules: + +[cols=",",options="header",] +|=== +|Module |Shared Use Case +|`+SafeAST+` |Common AST representation +|`+SafeType+` |Type system foundations +|`+SafeCompile+` |Compilation pipeline +|`+SafeError+` |Error handling patterns +|=== + +=== Implementation Strategy + +[arabic] +. *Core types*: Define common types in proven (SafeAST, SafeType) +. *Per-language extensions*: Each language adds its specific modules +. *Shared backend*: Compile proven modules to target runtimes +. *Cross-language proofs*: Use proven as proof interchange format + +=== Status + +* [ ] Define SafeAST for common representation +* [ ] Implement SafeLinear for Anvomidav +* [ ] Add SafePolicy for Phronesis +* [ ] Integrate SafeBounded for Oblíbený +* [ ] Create SafeEnergy for Eclexia diff --git a/extraction-queue/ephapax/design/proven-integration.md b/extraction-queue/ephapax/design/proven-integration.md deleted file mode 100644 index 384c7b9..0000000 --- a/extraction-queue/ephapax/design/proven-integration.md +++ /dev/null @@ -1,117 +0,0 @@ - -# Proven Library Integration Plan - -This document outlines how the [proven](https://github.com/hyperpolymath/proven) library's formally verified modules integrate with the Next-Gen Languages ecosystem. - -**Note:** Several Next-Gen Languages (especially Anvomidav and Duet) have formal verification as core features. The proven library provides shared verification infrastructure. - -## Per-Language Integration - -### Anvomidav (Formal Verification Focus) - -| Module | Use Case | Formal Guarantee | -|--------|----------|------------------| -| `SafeThm` | Theorem statement management | Well-typed propositions | -| `SafeLinear` | Linear type enforcement | Resource linearity | -| `SafeSession` | Session type checking | Protocol conformance | -| `SafeRealTime` | WCET analysis | Bounded execution time | - -Anvomidav's type system directly corresponds to proven modules: -- `Linear` → SafeLinear -- `Session` → SafeSession -- `@sched(EDF)` → SafeRealTime - -### Duet (AI-Assisted Verification) - -| Module | Use Case | Formal Guarantee | -|--------|----------|------------------| -| `SafeProperty` | Property synthesis targets | Valid specifications | -| `SafeThm` | AI-generated proof validation | Proof soundness | -| `SafeOracle` | AI verification oracle | Trusted computation | - -Duet's `@verify` and `@synth` annotations use proven as the verification backend. - -### Phronesis (AI Ethics/Alignment) - -| Module | Use Case | Formal Guarantee | -|--------|----------|------------------| -| `SafePolicy` | Ethical policy specification | Policy consistency | -| `SafeConstraint` | Value constraint checking | Constraint satisfaction | -| `SafeProvenance` | Decision audit trails | Accountability | - -Phronesis agents use SafePolicy for ethical framework specification. - -### Oblíbený (Secure Code) - -| Module | Use Case | Formal Guarantee | -|--------|----------|------------------| -| `SafeBounded` | Turing-incomplete enforcement | Termination guarantee | -| `SafeFlow` | Information flow control | No data leakage | -| `SafeCrypto` | Cryptographic operations | Correct algorithm usage | - -Oblíbený's `(forbid recursion)` maps to SafeBounded's termination proofs. - -### Eclexia (Resource-Constrained) - -| Module | Use Case | Formal Guarantee | -|--------|----------|------------------| -| `SafeResource` | Resource budget tracking | Budget compliance | -| `SafeEnergy` | Energy consumption proofs | Bounded energy use | -| `SafeMetric` | Resource metric validation | Valid measurements | - -Eclexia's `(energy budget ...)` uses SafeEnergy for compile-time verification. - -### Solo (Foundation Language) - -| Module | Use Case | Formal Guarantee | -|--------|----------|------------------| -| `SafeContract` | Pre/post conditions | Contract satisfaction | -| `SafeConcurrent` | Concurrency safety | Race-freedom | -| `SafeEffect` | Effect tracking | Effect containment | - -Solo's `where { pre: ..., post: ... }` uses SafeContract. - -### Ensemble (AI-Native) - -| Module | Use Case | Formal Guarantee | -|--------|----------|------------------| -| `SafeOracle` | AI model invocation | Trusted AI calls | -| `SafeEffect` | AI effect isolation | Effect boundaries | -| `SafeSchema` | Prompt validation | Well-formed prompts | - -### WokeLang (Human-Centric) - -| Module | Use Case | Formal Guarantee | -|--------|----------|------------------| -| `SafeConsent` | Consent tracking | Explicit consent | -| `SafePrivacy` | Privacy enforcement | Data protection | -| `SafeAccessibility` | A11y compliance | Accessibility checks | - -## Shared Infrastructure - -All Next-Gen Languages share these proven modules: - -| Module | Shared Use Case | -|--------|-----------------| -| `SafeAST` | Common AST representation | -| `SafeType` | Type system foundations | -| `SafeCompile` | Compilation pipeline | -| `SafeError` | Error handling patterns | - -## Implementation Strategy - -1. **Core types**: Define common types in proven (SafeAST, SafeType) -2. **Per-language extensions**: Each language adds its specific modules -3. **Shared backend**: Compile proven modules to target runtimes -4. **Cross-language proofs**: Use proven as proof interchange format - -## Status - -- [ ] Define SafeAST for common representation -- [ ] Implement SafeLinear for Anvomidav -- [ ] Add SafePolicy for Phronesis -- [ ] Integrate SafeBounded for Oblíbený -- [ ] Create SafeEnergy for Eclexia diff --git a/extraction-queue/ephapax/wiki-Ephapax.md b/extraction-queue/ephapax/wiki-Ephapax.adoc similarity index 83% rename from extraction-queue/ephapax/wiki-Ephapax.md rename to extraction-queue/ephapax/wiki-Ephapax.adoc index f4896eb..40309b2 100644 --- a/extraction-queue/ephapax/wiki-Ephapax.md +++ b/extraction-queue/ephapax/wiki-Ephapax.adoc @@ -1,27 +1,30 @@ - -# Ephapax +== Ephapax -**Tagline:** Once-only evaluation with linear semantics +*Tagline:* Once-only evaluation with linear semantics -## Overview +=== Overview -Ephapax (from Greek ἅπαξ "hapax" meaning "once") explores ephemeral, once-only computation. Values exist for a single use, enabling powerful guarantees about data flow, security, and resource management. +Ephapax (from Greek ἅπαξ "`hapax`" meaning "`once`") explores ephemeral, +once-only computation. Values exist for a single use, enabling powerful +guarantees about data flow, security, and resource management. -## Philosophy +=== Philosophy -In a world of persistent data and unlimited copying, Ephapax asks: what if values were precious, consumable, and finite? This constraint, far from being limiting, enables: +In a world of persistent data and unlimited copying, Ephapax asks: what +if values were precious, consumable, and finite? This constraint, far +from being limiting, enables: -- **Security**: Secrets can't be accidentally leaked (they're consumed on use) -- **Resource Safety**: Resources are guaranteed to be released -- **Protocol Verification**: Session types ensure correct communication patterns -- **Clarity**: Data flow is explicit and traceable +* *Security*: Secrets can’t be accidentally leaked (they’re consumed on +use) +* *Resource Safety*: Resources are guaranteed to be released +* *Protocol Verification*: Session types ensure correct communication +patterns +* *Clarity*: Data flow is explicit and traceable -## Quick Start +=== Quick Start -```scheme +[source,scheme] +---- ;; Hello World (println "Hello, Ephapax!") @@ -45,15 +48,16 @@ In a world of persistent data and unlimited copying, Ephapax asks: what if value (choice [(ok (recv Data) end)] [(err end)]))) -``` +---- -## Core Concepts +=== Core Concepts -### Once-Only Values +==== Once-Only Values -Values wrapped in `once` can be used exactly once: +Values wrapped in `+once+` can be used exactly once: -```scheme +[source,scheme] +---- ;; Create once-only value (define x (once 42)) @@ -66,13 +70,14 @@ Values wrapped in `once` can be used exactly once: ;; Pattern: transfer ownership (define (transfer-resource resource destination) (send destination (use resource))) ; resource consumed by send -``` +---- -### Ephemeral Computations +==== Ephemeral Computations Computations that produce one-time results: -```scheme +[source,scheme] +---- ;; Ephemeral lambda - can only be called once (define single-use-fn (ephemeral @@ -91,13 +96,14 @@ Computations that produce one-time results: (initialize) ; runs setup ; (initialize) ; ERROR: already initialized -``` +---- -### Linear Values +==== Linear Values Must be used exactly once (not zero, not more): -```scheme +[source,scheme] +---- ;; Linear resource (define (open-connection host) (linear (make-connection host))) @@ -116,13 +122,14 @@ Must be used exactly once (not zero, not more): (define (good-function) (let ((conn (open-connection "server"))) (pass-to-handler conn))) ; ownership transferred -``` +---- -### Affine Values +==== Affine Values Can be used at most once (can drop): -```scheme +[source,scheme] +---- ;; Affine value - optional use (define maybe-use (affine (expensive-compute))) @@ -136,13 +143,14 @@ Can be used at most once (can drop): (body file) ; file automatically cleaned up if not used )) -``` +---- -## Session Types +=== Session Types Protocol-correct communication: -```scheme +[source,scheme] +---- ;; Define protocol for authentication (define-session-type AuthProtocol (send String) ; client sends username @@ -170,13 +178,14 @@ Protocol-correct communication: ;; Type system ensures protocol is followed correctly ;; Cannot send when should receive, cannot skip steps -``` +---- -## Security Applications +=== Security Applications -### One-Time Tokens +==== One-Time Tokens -```scheme +[source,scheme] +---- ;; Generate one-time authentication token (define (generate-otp) (once (random-secure-string 32))) @@ -190,11 +199,12 @@ Protocol-correct communication: (authenticate-with-otp token) ; works ; (authenticate-with-otp token) ; ERROR: token consumed -``` +---- -### Secure Data Handling +==== Secure Data Handling -```scheme +[source,scheme] +---- ;; Sensitive data wrapper (define (sensitive data) (once @@ -211,11 +221,12 @@ Protocol-correct communication: ;; Cannot accidentally log or leak ; (println password) ; ERROR: cannot convert sensitive to string -``` +---- -### Capability Tokens +==== Capability Tokens -```scheme +[source,scheme] +---- ;; Issue capability for single action (define (issue-write-capability file) (once (make-capability 'write file))) @@ -229,13 +240,14 @@ Protocol-correct communication: (perform-write cap "important data") ; works ; (perform-write cap "more data") ; ERROR: capability consumed -``` +---- -## Resource Management +=== Resource Management -### File Handles +==== File Handles -```scheme +[source,scheme] +---- ;; Linear file handle (define (open-file path mode) (linear (system-open path mode))) @@ -254,11 +266,12 @@ Protocol-correct communication: (h3 contents (read-body h2)) ; h2 consumed, h3 returned (h4 (close-file h3))) ; h3 consumed contents)) -``` +---- -### Network Connections +==== Network Connections -```scheme +[source,scheme] +---- ;; Linear connection (define (connect host port) (linear (tcp-connect host port))) @@ -270,13 +283,14 @@ Protocol-correct communication: (c3 (send-line c2 "")) (c4 response (recv-response c3))) (values (close-connection c4) response))) -``` +---- -## Echidna Verification +=== Echidna Verification -### Protocol Verification +==== Protocol Verification -```scheme +[source,scheme] +---- ;; Verify session type compliance @verify (define-property session-type-safe @@ -285,22 +299,24 @@ Protocol-correct communication: (well-typed-session s))) ;; Echidna generates tests for all protocol paths -``` +---- -### Linearity Proofs +==== Linearity Proofs -```coq +[source,coq] +---- (* Prove linearity is preserved *) Theorem linearity_preservation : forall e v, linear_typed e -> e ⟶* v -> used_exactly_once e. -``` +---- -## Standard Library +=== Standard Library -```scheme +[source,scheme] +---- ;; Linear primitives (module ephapax/linear (once ; create once-only value @@ -334,11 +350,12 @@ Theorem linearity_preservation : with-capability ; use capability (consumes) delegate ; transfer capability attenuate)) ; create restricted sub-capability -``` +---- -## Example: Secure Messaging +=== Example: Secure Messaging -```scheme +[source,scheme] +---- (require ephapax/session) (require ephapax/secure) @@ -391,11 +408,11 @@ Theorem linearity_preservation : (chat-loop s''' (+ counter 1)))))) (chat-loop s2 0))) -``` +---- -## Related Pages +=== Related Pages -- [[Session Types]] -- [[Linear Logic]] -- [[Security Patterns]] -- [[Protocol Verification]] +* [link:#session-types[Session Types]] +* [[Linear Logic]] +* [[Security Patterns]] +* [link:#protocol-verification[Protocol Verification]] diff --git a/extraction-queue/jtv/wiki-jtv.adoc b/extraction-queue/jtv/wiki-jtv.adoc new file mode 100644 index 0000000..0516e28 --- /dev/null +++ b/extraction-queue/jtv/wiki-jtv.adoc @@ -0,0 +1,78 @@ +== jtv + +____ +Systems programming with Harvard Architecture +____ + +*Status:* 📝 Placeholder - contributions welcome + +=== Overview + +jtv is a systems programming language that enforces Harvard Architecture +principles: strict separation between code and data memory spaces. + +=== Core Invariant + +*Data and code occupy strictly separate memory spaces—no self-modifying +code.* + +=== Key Features + +* Code/data separation at language level +* Provably halting data transformations +* Static memory layout +* No runtime code generation + +=== Example + +[source,rust] +---- +// Data segment - immutable at runtime +data { + lookup_table: [u8; 256] = precomputed_values(), + constants: Config = load_config(), +} + +// Code segment - cannot write to data at runtime +code { + fn transform(input: u8) -> u8 { + data::lookup_table[input as usize] + } + + fn process(buffer: &[u8]) -> Vec { + buffer.iter().map(|b| transform(*b)).collect() + } +} +---- + +=== Security Benefits + +[cols=",",options="header",] +|=== +|Property |Benefit +|No code injection |Data can’t become code +|Predictable memory |Static layout analysis +|Cache optimization |Separate I-cache/D-cache +|Formal verification |Simpler memory model +|=== + +=== Use Cases + +* Embedded systems +* Security-critical code +* High-performance computing +* Firmware development + +=== Getting Started + +[source,bash] +---- +cd jtv +cargo run +---- + +=== See Also + +* [[Oblíbený]] - Security guarantees +* [[Anvomidav]] - Formal verification +* [[Solo Language]] - Systems foundation diff --git a/extraction-queue/jtv/wiki-jtv.md b/extraction-queue/jtv/wiki-jtv.md deleted file mode 100644 index 070623a..0000000 --- a/extraction-queue/jtv/wiki-jtv.md +++ /dev/null @@ -1,74 +0,0 @@ - -# jtv - -> Systems programming with Harvard Architecture - -**Status:** 📝 Placeholder - contributions welcome - -## Overview - -jtv is a systems programming language that enforces Harvard Architecture principles: strict separation between code and data memory spaces. - -## Core Invariant - -**Data and code occupy strictly separate memory spaces—no self-modifying code.** - -## Key Features - -- Code/data separation at language level -- Provably halting data transformations -- Static memory layout -- No runtime code generation - -## Example - -```rust -// Data segment - immutable at runtime -data { - lookup_table: [u8; 256] = precomputed_values(), - constants: Config = load_config(), -} - -// Code segment - cannot write to data at runtime -code { - fn transform(input: u8) -> u8 { - data::lookup_table[input as usize] - } - - fn process(buffer: &[u8]) -> Vec { - buffer.iter().map(|b| transform(*b)).collect() - } -} -``` - -## Security Benefits - -| Property | Benefit | -|----------|---------| -| No code injection | Data can't become code | -| Predictable memory | Static layout analysis | -| Cache optimization | Separate I-cache/D-cache | -| Formal verification | Simpler memory model | - -## Use Cases - -- Embedded systems -- Security-critical code -- High-performance computing -- Firmware development - -## Getting Started - -```bash -cd jtv -cargo run -``` - -## See Also - -- [[Oblíbený]] - Security guarantees -- [[Anvomidav]] - Formal verification -- [[Solo Language]] - Systems foundation diff --git a/extraction-queue/my-lang/wiki-Duet.adoc b/extraction-queue/my-lang/wiki-Duet.adoc new file mode 100644 index 0000000..b4b105a --- /dev/null +++ b/extraction-queue/my-lang/wiki-Duet.adoc @@ -0,0 +1,65 @@ +== Duet + +____ +AI-assisted development for verifiable software +____ + +*Status:* 📝 Placeholder - contributions welcome + +=== Overview + +Duet extends Solo with AI-assisted features, enabling a collaborative +relationship between human programmers and AI systems. Designed for ages +11-14. + +=== Core Invariant + +*AI-generated code is never trusted until formally verified.* + +=== Key Features + +* `+@synth+` - AI-powered code synthesis with verification +* `+@verify+` - Formal verification of code properties +* `+intent("...")+` - Natural language intent specification + +=== Example + +[source,duet] +---- +@synth +fn sort(list: List) -> List +where { + post: is_sorted(result) && is_permutation(result, list) +} +// AI synthesizes implementation, verified against contract + +@verify +fn binary_search(arr: List, target: Int) -> Option +where { + pre: is_sorted(arr) + post: result.is_some() implies arr[result.unwrap()] == target +} +{ + // Human-written, machine-verified +} +---- + +=== Getting Started + +[source,bash] +---- +cd my-lang +cargo run --bin duet +---- + +=== Neuro-Symbolic Integration + +See [[NEUROSYM.scm]] for details on how Duet bridges neural and symbolic +AI. + +=== See Also + +* [[My-Language Family]] +* [[Solo Language]] +* [[Ensemble Language]] +* [[Tutorial: Moving to Duet]] diff --git a/extraction-queue/my-lang/wiki-Duet.md b/extraction-queue/my-lang/wiki-Duet.md deleted file mode 100644 index 27ab932..0000000 --- a/extraction-queue/my-lang/wiki-Duet.md +++ /dev/null @@ -1,62 +0,0 @@ - -# Duet - -> AI-assisted development for verifiable software - -**Status:** 📝 Placeholder - contributions welcome - -## Overview - -Duet extends Solo with AI-assisted features, enabling a collaborative relationship between human programmers and AI systems. Designed for ages 11-14. - -## Core Invariant - -**AI-generated code is never trusted until formally verified.** - -## Key Features - -- `@synth` - AI-powered code synthesis with verification -- `@verify` - Formal verification of code properties -- `intent("...")` - Natural language intent specification - -## Example - -```duet -@synth -fn sort(list: List) -> List -where { - post: is_sorted(result) && is_permutation(result, list) -} -// AI synthesizes implementation, verified against contract - -@verify -fn binary_search(arr: List, target: Int) -> Option -where { - pre: is_sorted(arr) - post: result.is_some() implies arr[result.unwrap()] == target -} -{ - // Human-written, machine-verified -} -``` - -## Getting Started - -```bash -cd my-lang -cargo run --bin duet -``` - -## Neuro-Symbolic Integration - -See [[NEUROSYM.scm]] for details on how Duet bridges neural and symbolic AI. - -## See Also - -- [[My-Language Family]] -- [[Solo Language]] -- [[Ensemble Language]] -- [[Tutorial: Moving to Duet]] diff --git a/extraction-queue/my-lang/wiki-Ensemble.adoc b/extraction-queue/my-lang/wiki-Ensemble.adoc new file mode 100644 index 0000000..9cea89a --- /dev/null +++ b/extraction-queue/my-lang/wiki-Ensemble.adoc @@ -0,0 +1,66 @@ +== Ensemble + +____ +AI as a first-class, native component of the language +____ + +*Status:* 📝 Placeholder - contributions welcome + +=== Overview + +Ensemble treats AI models as fundamental building blocks of software, +not external services. Designed for ages 15-18 and professional use. + +=== Core Invariant + +*AI operations are tracked in the type system as effects.* + +=== Key Features + +* `+ai_model { ... }+` - First-class AI model definition +* `+prompt { ... }+` - Type-safe prompt construction +* `+AI+` - AI operations as typed effects + +=== Example + +[source,ensemble] +---- +ai_model Assistant { + provider: "claude" + capabilities: [text_generation, code_synthesis] + constraints: { max_tokens: 4096 } +} + +fn generate_summary(doc: Document) -> AI { + let prompt = prompt { + system: "You are a technical writer." + user: "Summarize: ${doc.content}" + } + + Assistant.complete(prompt) +} + +// AI effects are explicit in the return type +fn main() -> IO<()> { + let summary = run_ai(generate_summary(doc)) + print(summary) +} +---- + +=== Getting Started + +[source,bash] +---- +cd my-lang +cargo run --bin ensemble +---- + +=== Agent Development + +See [[AGENTIC.scm]] for agent-oriented patterns in Ensemble. + +=== See Also + +* [[My-Language Family]] +* [[Duet Language]] +* [[Tutorial: Mastering Ensemble]] diff --git a/extraction-queue/my-lang/wiki-Ensemble.md b/extraction-queue/my-lang/wiki-Ensemble.md deleted file mode 100644 index 88c7b4f..0000000 --- a/extraction-queue/my-lang/wiki-Ensemble.md +++ /dev/null @@ -1,65 +0,0 @@ - -# Ensemble - -> AI as a first-class, native component of the language - -**Status:** 📝 Placeholder - contributions welcome - -## Overview - -Ensemble treats AI models as fundamental building blocks of software, not external services. Designed for ages 15-18 and professional use. - -## Core Invariant - -**AI operations are tracked in the type system as effects.** - -## Key Features - -- `ai_model { ... }` - First-class AI model definition -- `prompt { ... }` - Type-safe prompt construction -- `AI` - AI operations as typed effects - -## Example - -```ensemble -ai_model Assistant { - provider: "claude" - capabilities: [text_generation, code_synthesis] - constraints: { max_tokens: 4096 } -} - -fn generate_summary(doc: Document) -> AI { - let prompt = prompt { - system: "You are a technical writer." - user: "Summarize: ${doc.content}" - } - - Assistant.complete(prompt) -} - -// AI effects are explicit in the return type -fn main() -> IO<()> { - let summary = run_ai(generate_summary(doc)) - print(summary) -} -``` - -## Getting Started - -```bash -cd my-lang -cargo run --bin ensemble -``` - -## Agent Development - -See [[AGENTIC.scm]] for agent-oriented patterns in Ensemble. - -## See Also - -- [[My-Language Family]] -- [[Duet Language]] -- [[Tutorial: Mastering Ensemble]] diff --git a/extraction-queue/my-lang/wiki-Me.adoc b/extraction-queue/my-lang/wiki-Me.adoc new file mode 100644 index 0000000..1251571 --- /dev/null +++ b/extraction-queue/my-lang/wiki-Me.adoc @@ -0,0 +1,79 @@ +== Me + +____ +Visual, playful introduction to programming +____ + +*Status:* 📝 Placeholder - contributions welcome + +____ +*Note (2026-06):* Me is *not* a fourth static dialect of the my-lang +family. The dialects are three and nested: Solo ⊂ Duet ⊂ Ensemble. Me is +an on-the-fly, *agent-generated projection* over that dialect hierarchy, +specified in `+tentacles-agentic-syllabus/me/README.adoc+`. Two earlier +attempts to build Me as a static dialect were retired +(`+hyperpolymath/me-dialect+` archived; the in-tree +`+my-lang/dialects/me/+` scaffolding sidelined). The block-language +sketch below predates that pivot and is kept for historical context. +____ + +=== Overview + +Me is the learner-facing entry point of the my-lang family. It +introduces computational thinking through visual/playful interaction, +generated as a projection rather than implemented as a standalone +compiler. + +=== Core Invariant + +*Every action has a visible, immediate result.* + +=== Key Features + +* Drag-and-drop blocks +* Immediate visual feedback +* Character-based narratives +* No syntax errors possible + +=== Concepts Introduced + +[cols=",",options="header",] +|=== +|Concept |Representation +|Sequence |Stacked blocks +|Repetition |Loop blocks with count +|Conditionals |Fork-in-road blocks +|Variables |Named containers +|=== + +=== Example (Block Description) + +.... +[When green flag clicked] + [Move forward 10 steps] + [Turn right 90 degrees] + [Repeat 4 times] + [Move forward 10 steps] + [Turn right 90 degrees] + [End repeat] +.... + +=== Getting Started + +The Me environment runs in a web browser. Visit the playground: + +https://github.com/hyperpolymath/language-playgrounds + +=== Progression + +Me is the first step in the [[My-Language Family]] progression: + +.... +Me (projection) → Solo (ages 8-10) → Duet (ages 11-14) → Ensemble (ages 15-18) +.... + +=== See Also + +* [[My-Language Family]] +* [[Solo Language]] +* [[Tutorial: Hello World]] diff --git a/extraction-queue/my-lang/wiki-Me.md b/extraction-queue/my-lang/wiki-Me.md deleted file mode 100644 index 81986f6..0000000 --- a/extraction-queue/my-lang/wiki-Me.md +++ /dev/null @@ -1,74 +0,0 @@ - -# Me - -> Visual, playful introduction to programming - -**Status:** 📝 Placeholder - contributions welcome - -> **Note (2026-06):** Me is **not** a fourth static dialect of the my-lang -> family. The dialects are three and nested: Solo ⊂ Duet ⊂ Ensemble. Me is an -> on-the-fly, **agent-generated projection** over that dialect hierarchy, -> specified in `tentacles-agentic-syllabus/me/README.adoc`. Two earlier -> attempts to build Me as a static dialect were retired -> (`hyperpolymath/me-dialect` archived; the in-tree `my-lang/dialects/me/` -> scaffolding sidelined). The block-language sketch below predates that -> pivot and is kept for historical context. - -## Overview - -Me is the learner-facing entry point of the my-lang family. It introduces computational thinking through visual/playful interaction, generated as a projection rather than implemented as a standalone compiler. - -## Core Invariant - -**Every action has a visible, immediate result.** - -## Key Features - -- Drag-and-drop blocks -- Immediate visual feedback -- Character-based narratives -- No syntax errors possible - -## Concepts Introduced - -| Concept | Representation | -|---------|----------------| -| Sequence | Stacked blocks | -| Repetition | Loop blocks with count | -| Conditionals | Fork-in-road blocks | -| Variables | Named containers | - -## Example (Block Description) - -``` -[When green flag clicked] - [Move forward 10 steps] - [Turn right 90 degrees] - [Repeat 4 times] - [Move forward 10 steps] - [Turn right 90 degrees] - [End repeat] -``` - -## Getting Started - -The Me environment runs in a web browser. Visit the playground: - -https://github.com/hyperpolymath/language-playgrounds - -## Progression - -Me is the first step in the [[My-Language Family]] progression: - -``` -Me (projection) → Solo (ages 8-10) → Duet (ages 11-14) → Ensemble (ages 15-18) -``` - -## See Also - -- [[My-Language Family]] -- [[Solo Language]] -- [[Tutorial: Hello World]] diff --git a/extraction-queue/my-lang/wiki-My-Language-Family.adoc b/extraction-queue/my-lang/wiki-My-Language-Family.adoc new file mode 100644 index 0000000..ee9f46a --- /dev/null +++ b/extraction-queue/my-lang/wiki-My-Language-Family.adoc @@ -0,0 +1,247 @@ +== My-Language Family + +The My-Language family is a progressive series of programming languages +designed to grow with learners from age 8 through age 18. + +=== Philosophy + +____ +"`Meet learners where they are, then guide them forward.`" +____ + +The family follows a *progressive disclosure* model: - Each language +builds on concepts from the previous - Complexity increases gradually - +Skills transfer seamlessly between levels - No "`unlearning`" required +when advancing + +=== The Languages + +____ +*Note (2026-06):* the dialects are three and *nested*: Solo ⊂ Duet ⊂ +Ensemble. Me is not a fourth dialect — it is an on-the-fly, +agent-generated projection over the dialect hierarchy (see +`+tentacles-agentic-syllabus/me/README.adoc+`). +____ + +.... +Me (agent-generated projection) + │ Visual, playful, purely exploratory + │ + ▼ +Solo (ages 8-10) + │ First text-based, simple syntax, immediate feedback + │ + ▼ +Duet (ages 11-14) + │ Collaborative features, expanded capabilities + │ + ▼ +Ensemble (ages 15-18) + │ Full-featured, industry-ready concepts + │ + ▼ +[Professional languages: Rust, Python, etc.] +.... + +=== Shared Characteristics + +All languages in the family share: + +==== Syntax Principles + +* *Readable keywords* (not cryptic symbols) +* *Consistent structure* across complexity levels +* *Minimal boilerplate* for beginners +* *Gradual typing* (optional types that become more prominent) + +==== Error Handling + +* *Friendly error messages* with suggestions +* *Age-appropriate explanations* +* *Visual error highlighting* +* *"`Did you mean…`" suggestions* + +==== Tooling + +* *Unified REPL* experience +* *Shared LSP* foundation +* *Cross-compatible packages* (where appropriate) +* *Consistent CLI* interface + +=== Progression Path + +==== Concepts Introduced by Level + +[width="100%",cols="29%,11%,14%,17%,29%",options="header",] +|=== +|Concept |Me |Solo |Duet |Ensemble +|Variables |Visual boxes |`+let x = 5+` |`+let x = 5+` +|`+let x: Int = 5+` + +|Output |Drag visual |`+say "Hi"+` |`+print("Hi")+` |`+println("Hi")+` + +|Loops |Repeat block |`+repeat 5 times+` |`+for i in 1..5+` +|`+for i in 1..=5+` + +|Functions |Action blocks |`+fun greet()+` |`+fn greet()+` +|`+fn greet() -> ()+` + +|Types |None |Implicit |Gradual |Static + +|Classes |None |None |Simple |Full OOP + +|Generics |None |None |None |Yes + +|Async |None |None |Basic |Full +|=== + +==== Skill Mapping + +.... +Solo Student Knows: Can Do in Duet: +───────────────────── ────────────────────── +Variables → Same, plus scope +Simple functions → Functions with params +repeat loops → for/while loops +Lists → Lists + dictionaries +───────────────────── ────────────────────── + +Duet Student Knows: Can Do in Ensemble: +───────────────────── ────────────────────── +Basic types → Full type system +Simple classes → Inheritance, traits +Basic async → Futures, streams +Module imports → Package management +───────────────────── ────────────────────── +.... + +=== Language Details + +==== [[Me Language]] + +* *Target age*: 6-8 +* *Paradigm*: Visual/block-based +* *Key feature*: No typing required, drag-and-drop +* *Environment*: Web playground only + +==== [[Solo Language]] + +* *Target age*: 8-10 +* *Paradigm*: Imperative, procedural +* *Key feature*: Simple syntax, immediate visual feedback +* *Environment*: Web playground, desktop REPL + +==== [[Duet Language]] + +* *Target age*: 11-14 +* *Paradigm*: Multi-paradigm (procedural + some OOP) +* *Key feature*: Collaborative coding, pair programming support +* *Environment*: Full IDE support, web, desktop + +==== [[Ensemble Language]] + +* *Target age*: 15-18 +* *Paradigm*: Full multi-paradigm +* *Key feature*: Industry-ready concepts, full type system +* *Environment*: Full toolchain, production deployable + +=== Related Repositories + +[width="100%",cols="58%,42%",options="header",] +|=== +|Repository |Purpose +|https://github.com/hyperpolymath/me[me] |Me language implementation + +|https://github.com/hyperpolymath/solo[solo] |Solo language +implementation + +|https://github.com/hyperpolymath/duet[duet] |Duet language +implementation + +|https://github.com/hyperpolymath/ensemble[ensemble] |Ensemble language +implementation + +|https://github.com/hyperpolymath/me-dialect-playground[me-dialect-playground] +|Experimental dialect features + +|https://github.com/hyperpolymath/my-newsroom[my-newsroom] |Content +pipeline + +|https://github.com/hyperpolymath/my-ssg[my-ssg] |Static site generator + +|https://github.com/hyperpolymath/tentacles-agentic-syllabus[tentacles-agentic-syllabus] +|Pedagogy: curriculum, syllabus, Me projector (previously +`+7-tentacles+`) +|=== + +=== Migration Between Languages + +==== Solo → Duet + +Most Solo code works in Duet with minor adjustments: + +[source,solo] +---- +// Solo +let name = "World" +say "Hello, " + name + +repeat 3 times + say "Hi!" +end +---- + +[source,duet] +---- +// Duet (equivalent) +let name = "World" +print("Hello, " + name) + +for _ in 1..3 { + print("Hi!") +} +---- + +==== Duet → Ensemble + +[source,duet] +---- +// Duet +fn greet(name) { + print("Hello, " + name) +} + +class Dog { + let name + + fn bark() { + print(self.name + " says woof!") + } +} +---- + +[source,ensemble] +---- +// Ensemble (equivalent) +fn greet(name: String) -> () { + println("Hello, {name}") +} + +struct Dog { + name: String, +} + +impl Dog { + fn bark(&self) -> () { + println("{} says woof!", self.name) + } +} +---- + +=== Educational Resources + +* [[Tutorial: Starting with Solo]] +* [[Tutorial: Moving to Duet]] +* [[Tutorial: Mastering Ensemble]] +* [[Curriculum Guide]] +* [[Teacher Resources]] diff --git a/extraction-queue/my-lang/wiki-My-Language-Family.md b/extraction-queue/my-lang/wiki-My-Language-Family.md deleted file mode 100644 index f1990fa..0000000 --- a/extraction-queue/my-lang/wiki-My-Language-Family.md +++ /dev/null @@ -1,208 +0,0 @@ - -# My-Language Family - -The My-Language family is a progressive series of programming languages designed to grow with learners from age 8 through age 18. - -## Philosophy - -> "Meet learners where they are, then guide them forward." - -The family follows a **progressive disclosure** model: -- Each language builds on concepts from the previous -- Complexity increases gradually -- Skills transfer seamlessly between levels -- No "unlearning" required when advancing - -## The Languages - -> **Note (2026-06):** the dialects are three and **nested**: -> Solo ⊂ Duet ⊂ Ensemble. Me is not a fourth dialect — it is an on-the-fly, -> agent-generated projection over the dialect hierarchy (see -> `tentacles-agentic-syllabus/me/README.adoc`). - -``` -Me (agent-generated projection) - │ Visual, playful, purely exploratory - │ - ▼ -Solo (ages 8-10) - │ First text-based, simple syntax, immediate feedback - │ - ▼ -Duet (ages 11-14) - │ Collaborative features, expanded capabilities - │ - ▼ -Ensemble (ages 15-18) - │ Full-featured, industry-ready concepts - │ - ▼ -[Professional languages: Rust, Python, etc.] -``` - -## Shared Characteristics - -All languages in the family share: - -### Syntax Principles -- **Readable keywords** (not cryptic symbols) -- **Consistent structure** across complexity levels -- **Minimal boilerplate** for beginners -- **Gradual typing** (optional types that become more prominent) - -### Error Handling -- **Friendly error messages** with suggestions -- **Age-appropriate explanations** -- **Visual error highlighting** -- **"Did you mean..." suggestions** - -### Tooling -- **Unified REPL** experience -- **Shared LSP** foundation -- **Cross-compatible packages** (where appropriate) -- **Consistent CLI** interface - -## Progression Path - -### Concepts Introduced by Level - -| Concept | Me | Solo | Duet | Ensemble | -|---------|----|----- |------|----------| -| Variables | Visual boxes | `let x = 5` | `let x = 5` | `let x: Int = 5` | -| Output | Drag visual | `say "Hi"` | `print("Hi")` | `println("Hi")` | -| Loops | Repeat block | `repeat 5 times` | `for i in 1..5` | `for i in 1..=5` | -| Functions | Action blocks | `fun greet()` | `fn greet()` | `fn greet() -> ()` | -| Types | None | Implicit | Gradual | Static | -| Classes | None | None | Simple | Full OOP | -| Generics | None | None | None | Yes | -| Async | None | None | Basic | Full | - -### Skill Mapping - -``` -Solo Student Knows: Can Do in Duet: -───────────────────── ────────────────────── -Variables → Same, plus scope -Simple functions → Functions with params -repeat loops → for/while loops -Lists → Lists + dictionaries -───────────────────── ────────────────────── - -Duet Student Knows: Can Do in Ensemble: -───────────────────── ────────────────────── -Basic types → Full type system -Simple classes → Inheritance, traits -Basic async → Futures, streams -Module imports → Package management -───────────────────── ────────────────────── -``` - -## Language Details - -### [[Me Language]] -- **Target age**: 6-8 -- **Paradigm**: Visual/block-based -- **Key feature**: No typing required, drag-and-drop -- **Environment**: Web playground only - -### [[Solo Language]] -- **Target age**: 8-10 -- **Paradigm**: Imperative, procedural -- **Key feature**: Simple syntax, immediate visual feedback -- **Environment**: Web playground, desktop REPL - -### [[Duet Language]] -- **Target age**: 11-14 -- **Paradigm**: Multi-paradigm (procedural + some OOP) -- **Key feature**: Collaborative coding, pair programming support -- **Environment**: Full IDE support, web, desktop - -### [[Ensemble Language]] -- **Target age**: 15-18 -- **Paradigm**: Full multi-paradigm -- **Key feature**: Industry-ready concepts, full type system -- **Environment**: Full toolchain, production deployable - -## Related Repositories - -| Repository | Purpose | -|------------|---------| -| [me](https://github.com/hyperpolymath/me) | Me language implementation | -| [solo](https://github.com/hyperpolymath/solo) | Solo language implementation | -| [duet](https://github.com/hyperpolymath/duet) | Duet language implementation | -| [ensemble](https://github.com/hyperpolymath/ensemble) | Ensemble language implementation | -| [me-dialect-playground](https://github.com/hyperpolymath/me-dialect-playground) | Experimental dialect features | -| [my-newsroom](https://github.com/hyperpolymath/my-newsroom) | Content pipeline | -| [my-ssg](https://github.com/hyperpolymath/my-ssg) | Static site generator | -| [tentacles-agentic-syllabus](https://github.com/hyperpolymath/tentacles-agentic-syllabus) | Pedagogy: curriculum, syllabus, Me projector (previously `7-tentacles`) | - -## Migration Between Languages - -### Solo → Duet - -Most Solo code works in Duet with minor adjustments: - -```solo -// Solo -let name = "World" -say "Hello, " + name - -repeat 3 times - say "Hi!" -end -``` - -```duet -// Duet (equivalent) -let name = "World" -print("Hello, " + name) - -for _ in 1..3 { - print("Hi!") -} -``` - -### Duet → Ensemble - -```duet -// Duet -fn greet(name) { - print("Hello, " + name) -} - -class Dog { - let name - - fn bark() { - print(self.name + " says woof!") - } -} -``` - -```ensemble -// Ensemble (equivalent) -fn greet(name: String) -> () { - println("Hello, {name}") -} - -struct Dog { - name: String, -} - -impl Dog { - fn bark(&self) -> () { - println("{} says woof!", self.name) - } -} -``` - -## Educational Resources - -- [[Tutorial: Starting with Solo]] -- [[Tutorial: Moving to Duet]] -- [[Tutorial: Mastering Ensemble]] -- [[Curriculum Guide]] -- [[Teacher Resources]] diff --git a/extraction-queue/my-lang/wiki-Solo.adoc b/extraction-queue/my-lang/wiki-Solo.adoc new file mode 100644 index 0000000..6a2d8c1 --- /dev/null +++ b/extraction-queue/my-lang/wiki-Solo.adoc @@ -0,0 +1,59 @@ +== Solo + +____ +Dependable foundation for systems programming +____ + +*Status:* 📝 Placeholder - contributions welcome + +=== Overview + +Solo is the foundational text-based language in the my-lang family, +designed for ages 8-10 as their first transition from visual to +text-based programming. + +=== Core Invariant + +*Effects are always explicit—no hidden side effects.* + +=== Key Features + +* `+effect { ... }+` - Explicit effect tracking +* `+go { ... }+` - Structured concurrency +* `+where { pre: ..., post: ... }+` - Design-by-contract + +=== Example + +[source,solo] +---- +fn greet(name: String) -> String + effect { console } + where { pre: name.length > 0 } +{ + console.print("Hello, ") + console.print(name) + return "greeted" +} +---- + +=== Getting Started + +[source,bash] +---- +cd my-lang +cargo run --bin solo +---- + +=== Progression + +Solo is part of the [[My-Language Family]] progression: + +.... +Me (projection) → Solo (ages 8-10) → Duet (ages 11-14) → Ensemble (ages 15-18) +.... + +=== See Also + +* [[My-Language Family]] +* [[Duet Language]] +* [[Tutorial: Starting with Solo]] diff --git a/extraction-queue/my-lang/wiki-Solo.md b/extraction-queue/my-lang/wiki-Solo.md deleted file mode 100644 index 8d19650..0000000 --- a/extraction-queue/my-lang/wiki-Solo.md +++ /dev/null @@ -1,57 +0,0 @@ - -# Solo - -> Dependable foundation for systems programming - -**Status:** 📝 Placeholder - contributions welcome - -## Overview - -Solo is the foundational text-based language in the my-lang family, designed for ages 8-10 as their first transition from visual to text-based programming. - -## Core Invariant - -**Effects are always explicit—no hidden side effects.** - -## Key Features - -- `effect { ... }` - Explicit effect tracking -- `go { ... }` - Structured concurrency -- `where { pre: ..., post: ... }` - Design-by-contract - -## Example - -```solo -fn greet(name: String) -> String - effect { console } - where { pre: name.length > 0 } -{ - console.print("Hello, ") - console.print(name) - return "greeted" -} -``` - -## Getting Started - -```bash -cd my-lang -cargo run --bin solo -``` - -## Progression - -Solo is part of the [[My-Language Family]] progression: - -``` -Me (projection) → Solo (ages 8-10) → Duet (ages 11-14) → Ensemble (ages 15-18) -``` - -## See Also - -- [[My-Language Family]] -- [[Duet Language]] -- [[Tutorial: Starting with Solo]] diff --git a/extraction-queue/oblibeny/wiki-Oblibeny.adoc b/extraction-queue/oblibeny/wiki-Oblibeny.adoc new file mode 100644 index 0000000..fee8eb3 --- /dev/null +++ b/extraction-queue/oblibeny/wiki-Oblibeny.adoc @@ -0,0 +1,78 @@ +== Oblíbený + +____ +Provably secure code for hostile environments +____ + +*Status:* 📝 Placeholder - contributions welcome + +=== Overview + +Oblíbený (Czech for "`favorite`" or "`beloved`") produces provably +secure, intentionally Turing-incomplete code for deployment in hostile +environments. By restricting expressiveness, it guarantees termination +and eliminates entire classes of vulnerabilities. + +=== Core Invariant + +*All programs must provably terminate—no unbounded recursion, no +infinite loops.* + +=== Key Features + +* `+(forbid recursion)+` - Explicit recursion prohibition +* `+(bounded-for ...)+` - Bounded iteration only +* Turing-incomplete by design +* Formal termination proofs + +=== Example + +[source,oblibeny] +---- +(module crypto-verify + (forbid recursion) + (forbid dynamic-allocation) + + (define (verify-signature sig msg key) + (bounded-for i 0 256 + (let byte (get-byte msg i)) + (accumulate (hash-step byte)))) + + (define (constant-time-compare a b) + (bounded-for i 0 32 + (xor-accumulate (get-byte a i) (get-byte b i))) + (is-zero? accumulator))) +---- + +=== Use Cases + +* Hardware Security Modules (HSMs) +* Secure enclaves (SGX, TrustZone) +* Smart card programming +* Cryptographic implementations +* High-assurance embedded systems + +=== Guarantees + +[cols=",",options="header",] +|=== +|Property |Guarantee +|Termination |Proven at compile time +|Memory safety |No dynamic allocation +|Timing safety |Constant-time operations +|Control flow |No indirect jumps +|=== + +=== Getting Started + +[source,bash] +---- +cd oblibeny +cargo run +---- + +=== See Also + +* [[Anvomidav]] - Real-time guarantees +* [[Eclexia]] - Resource constraints +* [[NEUROSYM.scm]] - Verification framework diff --git a/extraction-queue/oblibeny/wiki-Oblibeny.md b/extraction-queue/oblibeny/wiki-Oblibeny.md deleted file mode 100644 index 981a7b3..0000000 --- a/extraction-queue/oblibeny/wiki-Oblibeny.md +++ /dev/null @@ -1,72 +0,0 @@ - -# Oblíbený - -> Provably secure code for hostile environments - -**Status:** 📝 Placeholder - contributions welcome - -## Overview - -Oblíbený (Czech for "favorite" or "beloved") produces provably secure, intentionally Turing-incomplete code for deployment in hostile environments. By restricting expressiveness, it guarantees termination and eliminates entire classes of vulnerabilities. - -## Core Invariant - -**All programs must provably terminate—no unbounded recursion, no infinite loops.** - -## Key Features - -- `(forbid recursion)` - Explicit recursion prohibition -- `(bounded-for ...)` - Bounded iteration only -- Turing-incomplete by design -- Formal termination proofs - -## Example - -```oblibeny -(module crypto-verify - (forbid recursion) - (forbid dynamic-allocation) - - (define (verify-signature sig msg key) - (bounded-for i 0 256 - (let byte (get-byte msg i)) - (accumulate (hash-step byte)))) - - (define (constant-time-compare a b) - (bounded-for i 0 32 - (xor-accumulate (get-byte a i) (get-byte b i))) - (is-zero? accumulator))) -``` - -## Use Cases - -- Hardware Security Modules (HSMs) -- Secure enclaves (SGX, TrustZone) -- Smart card programming -- Cryptographic implementations -- High-assurance embedded systems - -## Guarantees - -| Property | Guarantee | -|----------|-----------| -| Termination | Proven at compile time | -| Memory safety | No dynamic allocation | -| Timing safety | Constant-time operations | -| Control flow | No indirect jumps | - -## Getting Started - -```bash -cd oblibeny -cargo run -``` - -## See Also - -- [[Anvomidav]] - Real-time guarantees -- [[Eclexia]] - Resource constraints -- [[NEUROSYM.scm]] - Verification framework diff --git a/extraction-queue/phronesis/wiki-Phronesis.adoc b/extraction-queue/phronesis/wiki-Phronesis.adoc new file mode 100644 index 0000000..34d050c --- /dev/null +++ b/extraction-queue/phronesis/wiki-Phronesis.adoc @@ -0,0 +1,71 @@ +== Phronesis + +____ +Formal specification of ethical AI frameworks +____ + +*Status:* 📝 Placeholder - contributions welcome + +=== Overview + +Named after the Aristotelian concept of practical wisdom, Phronesis +provides a formal, auditable language for specifying AI agent ethics. It +enables transparent reasoning about values, constraints, and +decision-making. + +=== Core Invariant + +*Every AI decision must be traceable to explicitly declared values.* + +=== Key Features + +* `+Agent.+` - Formal agent specification +* `+Values:+` - Explicit value hierarchy declaration +* `+EVALUATE(...)+` - Decision evaluation framework + +=== Example + +[source,phronesis] +---- +Agent.SafetyBot + Identity: + role: "Safety monitoring assistant" + scope: "Industrial automation" + + Values: + human_safety > property_protection > task_efficiency + transparency > speed + reversibility > finality + + Constraints: + MUST NOT take actions that risk human harm + MUST explain reasoning when asked + SHOULD prefer reversible actions + + EVALUATE(action) WHERE + risk_assessment(action) < acceptable_threshold + AND stakeholder_consent(action) = true + AND audit_log(action) = complete +---- + +=== Use Cases + +* AI safety research and alignment verification +* Regulatory compliance auditing +* Constitutional AI specification +* Ethical AI certification + +=== Getting Started + +[source,bash] +---- +cd phronesis +mix deps.get +mix run +---- + +=== See Also + +* [[AGENTIC.scm]] - Agent-oriented specifications +* [[Eclexia]] - Resource constraints (complementary) +* [[Anvomidav]] - Formal verification (complementary) diff --git a/extraction-queue/phronesis/wiki-Phronesis.md b/extraction-queue/phronesis/wiki-Phronesis.md deleted file mode 100644 index 0ca718b..0000000 --- a/extraction-queue/phronesis/wiki-Phronesis.md +++ /dev/null @@ -1,68 +0,0 @@ - -# Phronesis - -> Formal specification of ethical AI frameworks - -**Status:** 📝 Placeholder - contributions welcome - -## Overview - -Named after the Aristotelian concept of practical wisdom, Phronesis provides a formal, auditable language for specifying AI agent ethics. It enables transparent reasoning about values, constraints, and decision-making. - -## Core Invariant - -**Every AI decision must be traceable to explicitly declared values.** - -## Key Features - -- `Agent.` - Formal agent specification -- `Values:` - Explicit value hierarchy declaration -- `EVALUATE(...)` - Decision evaluation framework - -## Example - -```phronesis -Agent.SafetyBot - Identity: - role: "Safety monitoring assistant" - scope: "Industrial automation" - - Values: - human_safety > property_protection > task_efficiency - transparency > speed - reversibility > finality - - Constraints: - MUST NOT take actions that risk human harm - MUST explain reasoning when asked - SHOULD prefer reversible actions - - EVALUATE(action) WHERE - risk_assessment(action) < acceptable_threshold - AND stakeholder_consent(action) = true - AND audit_log(action) = complete -``` - -## Use Cases - -- AI safety research and alignment verification -- Regulatory compliance auditing -- Constitutional AI specification -- Ethical AI certification - -## Getting Started - -```bash -cd phronesis -mix deps.get -mix run -``` - -## See Also - -- [[AGENTIC.scm]] - Agent-oriented specifications -- [[Eclexia]] - Resource constraints (complementary) -- [[Anvomidav]] - Formal verification (complementary) diff --git a/extraction-queue/wokelang/wiki-WokeLang.adoc b/extraction-queue/wokelang/wiki-WokeLang.adoc new file mode 100644 index 0000000..4ba0f31 --- /dev/null +++ b/extraction-queue/wokelang/wiki-WokeLang.adoc @@ -0,0 +1,76 @@ +== WokeLang + +____ +Human-centric programming focused on consent and well-being +____ + +*Status:* 📝 Placeholder - contributions welcome + +=== Overview + +WokeLang prioritizes the human experience in programming. It uses +natural language constructs, explicit consent mechanisms, and supportive +error handling to make programming accessible and psychologically safe. + +=== Core Invariant + +*No sensitive operation executes without explicit user consent.* + +=== Key Features + +* `+only if okay "..."+` - Explicit consent for operations +* `+attempt ... or reassure+` - Supportive error recovery +* Natural language syntax +* Accessibility-first design + +=== Example + +[source,wokelang] +---- +// Consent-based data access +only if okay "May I access your location to show nearby events?" { + location = get_location() + events = find_events_near(location) + display(events) +} + +// Supportive error handling +attempt { + data = fetch_from_server() + process(data) +} or reassure "That's okay! The server seems busy right now. Would you like to try again, or shall we use cached data?" + +// Inclusive variable naming +let user_preference = ask "How would you like to be addressed?" +greet using user_preference +---- + +=== Design Principles + +[arabic] +. *Consent is explicit* - Never assume permission +. *Errors are supportive* - No blame, offer help +. *Language is inclusive* - Accessible to all +. *Feedback is constructive* - Guide, don’t criticize + +=== Use Cases + +* Educational programming for beginners +* Accessibility-focused applications +* Mental health technology +* Personal scripting +* Gentle introduction to coding + +=== Getting Started + +[source,bash] +---- +cd wokelang +cargo run +---- + +=== See Also + +* [[My-Language Family]] - Educational progression +* [[Tutorial: Hello World]] +* [[AGENTIC.scm]] - Human-agent interaction patterns diff --git a/extraction-queue/wokelang/wiki-WokeLang.md b/extraction-queue/wokelang/wiki-WokeLang.md deleted file mode 100644 index 724b638..0000000 --- a/extraction-queue/wokelang/wiki-WokeLang.md +++ /dev/null @@ -1,73 +0,0 @@ - -# WokeLang - -> Human-centric programming focused on consent and well-being - -**Status:** 📝 Placeholder - contributions welcome - -## Overview - -WokeLang prioritizes the human experience in programming. It uses natural language constructs, explicit consent mechanisms, and supportive error handling to make programming accessible and psychologically safe. - -## Core Invariant - -**No sensitive operation executes without explicit user consent.** - -## Key Features - -- `only if okay "..."` - Explicit consent for operations -- `attempt ... or reassure` - Supportive error recovery -- Natural language syntax -- Accessibility-first design - -## Example - -```wokelang -// Consent-based data access -only if okay "May I access your location to show nearby events?" { - location = get_location() - events = find_events_near(location) - display(events) -} - -// Supportive error handling -attempt { - data = fetch_from_server() - process(data) -} or reassure "That's okay! The server seems busy right now. Would you like to try again, or shall we use cached data?" - -// Inclusive variable naming -let user_preference = ask "How would you like to be addressed?" -greet using user_preference -``` - -## Design Principles - -1. **Consent is explicit** - Never assume permission -2. **Errors are supportive** - No blame, offer help -3. **Language is inclusive** - Accessible to all -4. **Feedback is constructive** - Guide, don't criticize - -## Use Cases - -- Educational programming for beginners -- Accessibility-focused applications -- Mental health technology -- Personal scripting -- Gentle introduction to coding - -## Getting Started - -```bash -cd wokelang -cargo run -``` - -## See Also - -- [[My-Language Family]] - Educational progression -- [[Tutorial: Hello World]] -- [[AGENTIC.scm]] - Human-agent interaction patterns diff --git a/languages/007.adoc b/languages/007.adoc new file mode 100644 index 0000000..2ba2d76 --- /dev/null +++ b/languages/007.adoc @@ -0,0 +1,26 @@ +== 007 — The Agent Meta-Language + +____ +Agents that make agents: every generated agent is itself a program in +the language. +____ + +*Status:* Specification *Classification:* Dual-Use Technology +(precautionary — anti-training-scrape measure) *Visibility:* Private +(standalone repo) *Repository:* `+The-Metadatastician/007+` (private) + +=== Summary + +A programming language for agents that make agents. Source code is in a +separate private repository to prevent training data scraping and +unauthorised replication. + +=== See + +Private repo: https://github.com/The-Metadatastician/007 + +This coordinator only _indexes_ the language; because the source is +deliberately private (anti-training-scrape), no implementation or +specification content is mirrored here. See also +link:../.machine_readable/LANGUAGES.a2ml[`+../.machine_readable/LANGUAGES.a2ml+`] +and link:../TOOLING-STATUS.adoc[`+../TOOLING-STATUS.adoc+`]. diff --git a/languages/007.md b/languages/007.md deleted file mode 100644 index b37bce9..0000000 --- a/languages/007.md +++ /dev/null @@ -1,27 +0,0 @@ - -# 007 — The Agent Meta-Language - -> Agents that make agents: every generated agent is itself a program in the language. - -**Status:** Specification -**Classification:** Dual-Use Technology (precautionary — anti-training-scrape measure) -**Visibility:** Private (standalone repo) -**Repository:** `The-Metadatastician/007` (private) - -## Summary - -A programming language for agents that make agents. Source code is in a -separate private repository to prevent training data scraping and -unauthorised replication. - -## See - -Private repo: https://github.com/The-Metadatastician/007 - -This coordinator only *indexes* the language; because the source is deliberately private -(anti-training-scrape), no implementation or specification content is mirrored here. See also -[`../.machine_readable/LANGUAGES.a2ml`](../.machine_readable/LANGUAGES.a2ml) and -[`../TOOLING-STATUS.adoc`](../TOOLING-STATUS.adoc). diff --git a/languages/README.adoc b/languages/README.adoc new file mode 100644 index 0000000..66bdcfd --- /dev/null +++ b/languages/README.adoc @@ -0,0 +1,51 @@ +== Language Quick Reference + +Each language has one core invariant that defines its design philosophy. + +[width="100%",cols="48%,52%",options="header",] +|=== +|Language |Invariant +|link:my-lang.md[my-lang] |Each level builds exactly on the previous + +|link:phronesis.md[phronesis] |Every AI decision traces to declared +values + +|link:eclexia.md[eclexia] |No computation without explicit resource +budget + +|link:oblibeny.md[oblibeny] |All programs must provably terminate + +|link:anvomidav.md[anvomidav] |Every deadline is statically guaranteed + +|link:wokelang.md[wokelang] |No operation without explicit consent + +|link:betlang.md[betlang] |All uncertainty must be explicitly modeled + +|link:jtv.md[jtv] |Data and code are strictly separated + +|link:affinescript.md[affinescript] |Every resource is used at most once + +|link:ephapax.md[ephapax] |Every value can be consumed exactly once + +|link:haec.md[haec] |Every quality-loss is graded and checked against +its use + +|link:error-lang.md[error-lang] |Errors are first-class: systems +thinking taught through failure + +|link:tangle.md[tangle] |Programs are braids; equivalence is topological +isotopy + +|link:007.md[007] |Agents that make agents (private repo, anti-scrape; +index-only) + +|link:kitchenspeak.md[kitchenspeak] |Physical-process constraints are +enforced in the types +|=== + +Each row links to a thin pointer; the language itself lives in its own +`+hyperpolymath/+` repo. For cross-language status see +link:../TOOLING-STATUS.adoc[`+../TOOLING-STATUS.adoc+`], +link:../.machine_readable/LANGUAGES.a2ml[`+../.machine_readable/LANGUAGES.a2ml+`], +and +link:../language-status-tracker.jl[`+../language-status-tracker.jl+`]. diff --git a/languages/README.md b/languages/README.md deleted file mode 100644 index 1009f20..0000000 --- a/languages/README.md +++ /dev/null @@ -1,31 +0,0 @@ - -# Language Quick Reference - -Each language has one core invariant that defines its design philosophy. - -| Language | Invariant | -|----------|-----------| -| [my-lang](my-lang.md) | Each level builds exactly on the previous | -| [phronesis](phronesis.md) | Every AI decision traces to declared values | -| [eclexia](eclexia.md) | No computation without explicit resource budget | -| [oblibeny](oblibeny.md) | All programs must provably terminate | -| [anvomidav](anvomidav.md) | Every deadline is statically guaranteed | -| [wokelang](wokelang.md) | No operation without explicit consent | -| [betlang](betlang.md) | All uncertainty must be explicitly modeled | -| [jtv](jtv.md) | Data and code are strictly separated | -| [affinescript](affinescript.md) | Every resource is used at most once | -| [ephapax](ephapax.md) | Every value can be consumed exactly once | -| [haec](haec.md) | Every quality-loss is graded and checked against its use | -| [error-lang](error-lang.md) | Errors are first-class: systems thinking taught through failure | -| [tangle](tangle.md) | Programs are braids; equivalence is topological isotopy | -| [007](007.md) | Agents that make agents (private repo, anti-scrape; index-only) | -| [kitchenspeak](kitchenspeak.md) | Physical-process constraints are enforced in the types | - -Each row links to a thin pointer; the language itself lives in its own -`hyperpolymath/` repo. For cross-language status see -[`../TOOLING-STATUS.adoc`](../TOOLING-STATUS.adoc), -[`../.machine_readable/LANGUAGES.a2ml`](../.machine_readable/LANGUAGES.a2ml), and -[`../language-status-tracker.jl`](../language-status-tracker.jl). diff --git a/languages/affinescript.adoc b/languages/affinescript.adoc new file mode 100644 index 0000000..7e3ec0e --- /dev/null +++ b/languages/affinescript.adoc @@ -0,0 +1,14 @@ +== AffineScript + +____ +Every resource is used at most once. +____ + +*Canonical repository:* +https://github.com/hyperpolymath/affinescript[hyperpolymath/affinescript] + +This coordinator only _indexes_ the language. The implementation, +specification, grammar, examples, and live status live in the canonical +repository above — not here. See also +link:../.machine_readable/LANGUAGES.a2ml[`+../.machine_readable/LANGUAGES.a2ml+`] +and link:../TOOLING-STATUS.adoc[`+../TOOLING-STATUS.adoc+`]. diff --git a/languages/affinescript.md b/languages/affinescript.md deleted file mode 100644 index d0fd7d5..0000000 --- a/languages/affinescript.md +++ /dev/null @@ -1,14 +0,0 @@ - -# AffineScript - -> Every resource is used at most once. - -**Canonical repository:** [hyperpolymath/affinescript](https://github.com/hyperpolymath/affinescript) - -This coordinator only *indexes* the language. The implementation, specification, grammar, -examples, and live status live in the canonical repository above — not here. See also -[`../.machine_readable/LANGUAGES.a2ml`](../.machine_readable/LANGUAGES.a2ml) and -[`../TOOLING-STATUS.adoc`](../TOOLING-STATUS.adoc). diff --git a/languages/anvomidav.adoc b/languages/anvomidav.adoc new file mode 100644 index 0000000..ecb5230 --- /dev/null +++ b/languages/anvomidav.adoc @@ -0,0 +1,14 @@ +== Anvomidav + +____ +Every deadline is statically guaranteed. +____ + +*Canonical repository:* +https://github.com/hyperpolymath/anvomidav[hyperpolymath/anvomidav] + +This coordinator only _indexes_ the language. The implementation, +specification, grammar, examples, and live status live in the canonical +repository above — not here. See also +link:../.machine_readable/LANGUAGES.a2ml[`+../.machine_readable/LANGUAGES.a2ml+`] +and link:../TOOLING-STATUS.adoc[`+../TOOLING-STATUS.adoc+`]. diff --git a/languages/anvomidav.md b/languages/anvomidav.md deleted file mode 100644 index 9b6e9d3..0000000 --- a/languages/anvomidav.md +++ /dev/null @@ -1,14 +0,0 @@ - -# Anvomidav - -> Every deadline is statically guaranteed. - -**Canonical repository:** [hyperpolymath/anvomidav](https://github.com/hyperpolymath/anvomidav) - -This coordinator only *indexes* the language. The implementation, specification, grammar, -examples, and live status live in the canonical repository above — not here. See also -[`../.machine_readable/LANGUAGES.a2ml`](../.machine_readable/LANGUAGES.a2ml) and -[`../TOOLING-STATUS.adoc`](../TOOLING-STATUS.adoc). diff --git a/languages/betlang.adoc b/languages/betlang.adoc new file mode 100644 index 0000000..a5e8b78 --- /dev/null +++ b/languages/betlang.adoc @@ -0,0 +1,14 @@ +== betlang + +____ +All uncertainty must be explicitly modeled. +____ + +*Canonical repository:* +https://github.com/hyperpolymath/betlang[hyperpolymath/betlang] + +This coordinator only _indexes_ the language. The implementation, +specification, grammar, examples, and live status live in the canonical +repository above — not here. See also +link:../.machine_readable/LANGUAGES.a2ml[`+../.machine_readable/LANGUAGES.a2ml+`] +and link:../TOOLING-STATUS.adoc[`+../TOOLING-STATUS.adoc+`]. diff --git a/languages/betlang.md b/languages/betlang.md deleted file mode 100644 index 8bc3aa2..0000000 --- a/languages/betlang.md +++ /dev/null @@ -1,14 +0,0 @@ - -# betlang - -> All uncertainty must be explicitly modeled. - -**Canonical repository:** [hyperpolymath/betlang](https://github.com/hyperpolymath/betlang) - -This coordinator only *indexes* the language. The implementation, specification, grammar, -examples, and live status live in the canonical repository above — not here. See also -[`../.machine_readable/LANGUAGES.a2ml`](../.machine_readable/LANGUAGES.a2ml) and -[`../TOOLING-STATUS.adoc`](../TOOLING-STATUS.adoc). diff --git a/languages/eclexia.adoc b/languages/eclexia.adoc new file mode 100644 index 0000000..7fbd369 --- /dev/null +++ b/languages/eclexia.adoc @@ -0,0 +1,14 @@ +== Eclexia + +____ +No computation without explicit resource budget. +____ + +*Canonical repository:* +https://github.com/hyperpolymath/eclexia[hyperpolymath/eclexia] + +This coordinator only _indexes_ the language. The implementation, +specification, grammar, examples, and live status live in the canonical +repository above — not here. See also +link:../.machine_readable/LANGUAGES.a2ml[`+../.machine_readable/LANGUAGES.a2ml+`] +and link:../TOOLING-STATUS.adoc[`+../TOOLING-STATUS.adoc+`]. diff --git a/languages/eclexia.md b/languages/eclexia.md deleted file mode 100644 index 78f143f..0000000 --- a/languages/eclexia.md +++ /dev/null @@ -1,14 +0,0 @@ - -# Eclexia - -> No computation without explicit resource budget. - -**Canonical repository:** [hyperpolymath/eclexia](https://github.com/hyperpolymath/eclexia) - -This coordinator only *indexes* the language. The implementation, specification, grammar, -examples, and live status live in the canonical repository above — not here. See also -[`../.machine_readable/LANGUAGES.a2ml`](../.machine_readable/LANGUAGES.a2ml) and -[`../TOOLING-STATUS.adoc`](../TOOLING-STATUS.adoc). diff --git a/languages/ephapax.adoc b/languages/ephapax.adoc new file mode 100644 index 0000000..6c4fa49 --- /dev/null +++ b/languages/ephapax.adoc @@ -0,0 +1,14 @@ +== Ephapax + +____ +Every value can be consumed exactly once. +____ + +*Canonical repository:* +https://github.com/hyperpolymath/ephapax[hyperpolymath/ephapax] + +This coordinator only _indexes_ the language. The implementation, +specification, grammar, examples, and live status live in the canonical +repository above — not here. See also +link:../.machine_readable/LANGUAGES.a2ml[`+../.machine_readable/LANGUAGES.a2ml+`] +and link:../TOOLING-STATUS.adoc[`+../TOOLING-STATUS.adoc+`]. diff --git a/languages/ephapax.md b/languages/ephapax.md deleted file mode 100644 index 3573669..0000000 --- a/languages/ephapax.md +++ /dev/null @@ -1,14 +0,0 @@ - -# Ephapax - -> Every value can be consumed exactly once. - -**Canonical repository:** [hyperpolymath/ephapax](https://github.com/hyperpolymath/ephapax) - -This coordinator only *indexes* the language. The implementation, specification, grammar, -examples, and live status live in the canonical repository above — not here. See also -[`../.machine_readable/LANGUAGES.a2ml`](../.machine_readable/LANGUAGES.a2ml) and -[`../TOOLING-STATUS.adoc`](../TOOLING-STATUS.adoc). diff --git a/languages/error-lang.adoc b/languages/error-lang.adoc new file mode 100644 index 0000000..c97155c --- /dev/null +++ b/languages/error-lang.adoc @@ -0,0 +1,18 @@ +== Error-Lang + +____ +Errors are first-class: systems thinking is taught through failure. +____ + +*Canonical repository:* +https://github.com/hyperpolymath/error-lang[hyperpolymath/error-lang] + +A pedagogical language that teaches systems thinking by making errors +the primary object of study rather than an afterthought — every failure +mode is a named, first-class value the learner reasons about explicitly. + +This coordinator only _indexes_ the language. The implementation, +specification, grammar, examples, and live status live in the canonical +repository above — not here. See also +link:../.machine_readable/LANGUAGES.a2ml[`+../.machine_readable/LANGUAGES.a2ml+`] +and link:../TOOLING-STATUS.adoc[`+../TOOLING-STATUS.adoc+`]. diff --git a/languages/error-lang.md b/languages/error-lang.md deleted file mode 100644 index 5c3c70d..0000000 --- a/languages/error-lang.md +++ /dev/null @@ -1,18 +0,0 @@ - -# Error-Lang - -> Errors are first-class: systems thinking is taught through failure. - -**Canonical repository:** [hyperpolymath/error-lang](https://github.com/hyperpolymath/error-lang) - -A pedagogical language that teaches systems thinking by making errors the primary -object of study rather than an afterthought — every failure mode is a named, -first-class value the learner reasons about explicitly. - -This coordinator only *indexes* the language. The implementation, specification, grammar, -examples, and live status live in the canonical repository above — not here. See also -[`../.machine_readable/LANGUAGES.a2ml`](../.machine_readable/LANGUAGES.a2ml) and -[`../TOOLING-STATUS.adoc`](../TOOLING-STATUS.adoc). diff --git a/languages/haec.adoc b/languages/haec.adoc new file mode 100644 index 0000000..f637839 --- /dev/null +++ b/languages/haec.adoc @@ -0,0 +1,34 @@ +== Haec + +____ +Every quality-loss is graded and checked against its use. +____ + +*Canonical repository:* +https://github.com/hyperpolymath/haec[hyperpolymath/haec] + +Haec is a Turing-complete language whose type discipline is +_trope-particularity_: every operation on a _property-instance_ (a +quality as borne by _this_ entity, in _this_ context) carries a +_loss-shape grade_, and the surviving residue is judged against a +declared _use-model_. Haec is one *front-end* of a three-repo system — +it lowers programs to a language-neutral *Trope IR*; it defines neither +the checker nor the vocabulary: + +* https://github.com/hyperpolymath/trope-checker[hyperpolymath/trope-checker] +— the portable checker (Idris2 verified core + executable) that consumes +the Trope IR and returns a verdict (`+p-sufficient+` / +`+p-insufficient+`) with a witness edge. +* https://github.com/hyperpolymath/trope-particularity-workbench[hyperpolymath/trope-particularity-workbench] +— the informal vocabulary (the nine named effects, the residual, the +verdict). + +Shares the _irreversible-transformation-with-retained-residue_ substrate +with https://github.com/hyperpolymath/echo-types[`+echo-types+`] (the +graded-loss reading the calculus builds on). + +This coordinator only _indexes_ the language. The implementation, +specification, grammar, examples, and live status live in the canonical +repositories above — not here. See also +link:../.machine_readable/LANGUAGES.a2ml[`+../.machine_readable/LANGUAGES.a2ml+`] +and link:../TOOLING-STATUS.adoc[`+../TOOLING-STATUS.adoc+`]. diff --git a/languages/haec.md b/languages/haec.md deleted file mode 100644 index 2b97edc..0000000 --- a/languages/haec.md +++ /dev/null @@ -1,31 +0,0 @@ - -# Haec - -> Every quality-loss is graded and checked against its use. - -**Canonical repository:** [hyperpolymath/haec](https://github.com/hyperpolymath/haec) - -Haec is a Turing-complete language whose type discipline is *trope-particularity*: -every operation on a *property-instance* (a quality as borne by _this_ entity, in -_this_ context) carries a *loss-shape grade*, and the surviving residue is judged -against a declared *use-model*. Haec is one **front-end** of a three-repo system — -it lowers programs to a language-neutral **Trope IR**; it defines neither the -checker nor the vocabulary: - -- [hyperpolymath/trope-checker](https://github.com/hyperpolymath/trope-checker) — - the portable checker (Idris2 verified core + executable) that consumes the Trope - IR and returns a verdict (`p-sufficient` / `p-insufficient`) with a witness edge. -- [hyperpolymath/trope-particularity-workbench](https://github.com/hyperpolymath/trope-particularity-workbench) — - the informal vocabulary (the nine named effects, the residual, the verdict). - -Shares the *irreversible-transformation-with-retained-residue* substrate with -[`echo-types`](https://github.com/hyperpolymath/echo-types) (the graded-loss reading -the calculus builds on). - -This coordinator only *indexes* the language. The implementation, specification, -grammar, examples, and live status live in the canonical repositories above — not -here. See also [`../.machine_readable/LANGUAGES.a2ml`](../.machine_readable/LANGUAGES.a2ml) -and [`../TOOLING-STATUS.adoc`](../TOOLING-STATUS.adoc). diff --git a/languages/jtv.adoc b/languages/jtv.adoc new file mode 100644 index 0000000..1652cc2 --- /dev/null +++ b/languages/jtv.adoc @@ -0,0 +1,14 @@ +== JtV + +____ +Data and code are strictly separated. +____ + +*Canonical repository:* +https://github.com/hyperpolymath/jtv[hyperpolymath/jtv] + +This coordinator only _indexes_ the language. The implementation, +specification, grammar, examples, and live status live in the canonical +repository above — not here. See also +link:../.machine_readable/LANGUAGES.a2ml[`+../.machine_readable/LANGUAGES.a2ml+`] +and link:../TOOLING-STATUS.adoc[`+../TOOLING-STATUS.adoc+`]. diff --git a/languages/jtv.md b/languages/jtv.md deleted file mode 100644 index 9ec7d33..0000000 --- a/languages/jtv.md +++ /dev/null @@ -1,14 +0,0 @@ - -# JtV - -> Data and code are strictly separated. - -**Canonical repository:** [hyperpolymath/jtv](https://github.com/hyperpolymath/jtv) - -This coordinator only *indexes* the language. The implementation, specification, grammar, -examples, and live status live in the canonical repository above — not here. See also -[`../.machine_readable/LANGUAGES.a2ml`](../.machine_readable/LANGUAGES.a2ml) and -[`../TOOLING-STATUS.adoc`](../TOOLING-STATUS.adoc). diff --git a/languages/kitchenspeak.adoc b/languages/kitchenspeak.adoc new file mode 100644 index 0000000..1fef27f --- /dev/null +++ b/languages/kitchenspeak.adoc @@ -0,0 +1,22 @@ +== KitchenSpeak + +____ +Physical-process constraints are enforced in the types +(physics-in-types). +____ + +*Canonical repository:* +https://github.com/hyperpolymath/kitchenspeak[hyperpolymath/kitchenspeak] + +An experimental kitchen-orchestration DSL. The in-tree v1.0 snapshot was +extracted 2026-06 (see +link:../EXTRACTION-MANIFEST.md[`+../EXTRACTION-MANIFEST.md+`]); the +standalone repo carries the superseding v2.0 (physics-in-types, OCaml +compiler, machine-checked Agda) and consumes the +https://github.com/hyperpolymath/echo-types[`+echo-types+`] substrate. + +This coordinator only _indexes_ the language. The implementation, +specification, grammar, examples, and live status live in the canonical +repository above — not here. See also +link:../.machine_readable/LANGUAGES.a2ml[`+../.machine_readable/LANGUAGES.a2ml+`] +and link:../TOOLING-STATUS.adoc[`+../TOOLING-STATUS.adoc+`]. diff --git a/languages/kitchenspeak.md b/languages/kitchenspeak.md deleted file mode 100644 index 84e6810..0000000 --- a/languages/kitchenspeak.md +++ /dev/null @@ -1,20 +0,0 @@ - -# KitchenSpeak - -> Physical-process constraints are enforced in the types (physics-in-types). - -**Canonical repository:** [hyperpolymath/kitchenspeak](https://github.com/hyperpolymath/kitchenspeak) - -An experimental kitchen-orchestration DSL. The in-tree v1.0 snapshot was extracted -2026-06 (see [`../EXTRACTION-MANIFEST.md`](../EXTRACTION-MANIFEST.md)); the standalone -repo carries the superseding v2.0 (physics-in-types, OCaml compiler, machine-checked -Agda) and consumes the [`echo-types`](https://github.com/hyperpolymath/echo-types) -substrate. - -This coordinator only *indexes* the language. The implementation, specification, grammar, -examples, and live status live in the canonical repository above — not here. See also -[`../.machine_readable/LANGUAGES.a2ml`](../.machine_readable/LANGUAGES.a2ml) and -[`../TOOLING-STATUS.adoc`](../TOOLING-STATUS.adoc). diff --git a/languages/my-lang.adoc b/languages/my-lang.adoc new file mode 100644 index 0000000..e92ec48 --- /dev/null +++ b/languages/my-lang.adoc @@ -0,0 +1,14 @@ +== My-Lang + +____ +Each level builds exactly on the previous. +____ + +*Canonical repository:* +https://github.com/hyperpolymath/my-lang[hyperpolymath/my-lang] + +This coordinator only _indexes_ the language. The implementation, +specification, grammar, examples, and live status live in the canonical +repository above — not here. See also +link:../.machine_readable/LANGUAGES.a2ml[`+../.machine_readable/LANGUAGES.a2ml+`] +and link:../TOOLING-STATUS.adoc[`+../TOOLING-STATUS.adoc+`]. diff --git a/languages/my-lang.md b/languages/my-lang.md deleted file mode 100644 index 896dbda..0000000 --- a/languages/my-lang.md +++ /dev/null @@ -1,14 +0,0 @@ - -# My-Lang - -> Each level builds exactly on the previous. - -**Canonical repository:** [hyperpolymath/my-lang](https://github.com/hyperpolymath/my-lang) - -This coordinator only *indexes* the language. The implementation, specification, grammar, -examples, and live status live in the canonical repository above — not here. See also -[`../.machine_readable/LANGUAGES.a2ml`](../.machine_readable/LANGUAGES.a2ml) and -[`../TOOLING-STATUS.adoc`](../TOOLING-STATUS.adoc). diff --git a/languages/oblibeny.adoc b/languages/oblibeny.adoc new file mode 100644 index 0000000..7a11635 --- /dev/null +++ b/languages/oblibeny.adoc @@ -0,0 +1,14 @@ +== Oblíbený + +____ +All programs must provably terminate. +____ + +*Canonical repository:* +https://github.com/hyperpolymath/oblibeny[hyperpolymath/oblibeny] + +This coordinator only _indexes_ the language. The implementation, +specification, grammar, examples, and live status live in the canonical +repository above — not here. See also +link:../.machine_readable/LANGUAGES.a2ml[`+../.machine_readable/LANGUAGES.a2ml+`] +and link:../TOOLING-STATUS.adoc[`+../TOOLING-STATUS.adoc+`]. diff --git a/languages/oblibeny.md b/languages/oblibeny.md deleted file mode 100644 index 7a8c7f8..0000000 --- a/languages/oblibeny.md +++ /dev/null @@ -1,14 +0,0 @@ - -# Oblíbený - -> All programs must provably terminate. - -**Canonical repository:** [hyperpolymath/oblibeny](https://github.com/hyperpolymath/oblibeny) - -This coordinator only *indexes* the language. The implementation, specification, grammar, -examples, and live status live in the canonical repository above — not here. See also -[`../.machine_readable/LANGUAGES.a2ml`](../.machine_readable/LANGUAGES.a2ml) and -[`../TOOLING-STATUS.adoc`](../TOOLING-STATUS.adoc). diff --git a/languages/phronesis.adoc b/languages/phronesis.adoc new file mode 100644 index 0000000..3b232a6 --- /dev/null +++ b/languages/phronesis.adoc @@ -0,0 +1,14 @@ +== Phronesis + +____ +Every AI decision traces to declared values. +____ + +*Canonical repository:* +https://github.com/hyperpolymath/phronesis[hyperpolymath/phronesis] + +This coordinator only _indexes_ the language. The implementation, +specification, grammar, examples, and live status live in the canonical +repository above — not here. See also +link:../.machine_readable/LANGUAGES.a2ml[`+../.machine_readable/LANGUAGES.a2ml+`] +and link:../TOOLING-STATUS.adoc[`+../TOOLING-STATUS.adoc+`]. diff --git a/languages/phronesis.md b/languages/phronesis.md deleted file mode 100644 index fc02996..0000000 --- a/languages/phronesis.md +++ /dev/null @@ -1,14 +0,0 @@ - -# Phronesis - -> Every AI decision traces to declared values. - -**Canonical repository:** [hyperpolymath/phronesis](https://github.com/hyperpolymath/phronesis) - -This coordinator only *indexes* the language. The implementation, specification, grammar, -examples, and live status live in the canonical repository above — not here. See also -[`../.machine_readable/LANGUAGES.a2ml`](../.machine_readable/LANGUAGES.a2ml) and -[`../TOOLING-STATUS.adoc`](../TOOLING-STATUS.adoc). diff --git a/languages/tangle.adoc b/languages/tangle.adoc new file mode 100644 index 0000000..a9016ec --- /dev/null +++ b/languages/tangle.adoc @@ -0,0 +1,22 @@ +== Tangle + +____ +Programs are braids; equivalence is topological isotopy. +____ + +*Canonical repository:* +https://github.com/hyperpolymath/tangle[hyperpolymath/tangle] + +A topologically inspired language: programs are represented as +knots/braids and program equivalence is defined by isotopy. The core +type system is mechanised in Lean. Tangle’s IR (*TangleIR*) is also the +canonical representation consumed by the separate *KRL resolution stack* +(`+krl → TangleIR → VeriSimCore → Skein.jl / quandledb+`) — that +database/resolution stack is tracked by the database estate, not by this +coordinator. + +This coordinator only _indexes_ the language. The implementation, +specification, grammar, examples, and live status live in the canonical +repository above — not here. See also +link:../.machine_readable/LANGUAGES.a2ml[`+../.machine_readable/LANGUAGES.a2ml+`] +and link:../TOOLING-STATUS.adoc[`+../TOOLING-STATUS.adoc+`]. diff --git a/languages/tangle.md b/languages/tangle.md deleted file mode 100644 index 1c7c616..0000000 --- a/languages/tangle.md +++ /dev/null @@ -1,21 +0,0 @@ - -# Tangle - -> Programs are braids; equivalence is topological isotopy. - -**Canonical repository:** [hyperpolymath/tangle](https://github.com/hyperpolymath/tangle) - -A topologically inspired language: programs are represented as knots/braids and -program equivalence is defined by isotopy. The core type system is mechanised in -Lean. Tangle's IR (**TangleIR**) is also the canonical representation consumed by -the separate **KRL resolution stack** (`krl → TangleIR → VeriSimCore → Skein.jl / -quandledb`) — that database/resolution stack is tracked by the database estate, not -by this coordinator. - -This coordinator only *indexes* the language. The implementation, specification, grammar, -examples, and live status live in the canonical repository above — not here. See also -[`../.machine_readable/LANGUAGES.a2ml`](../.machine_readable/LANGUAGES.a2ml) and -[`../TOOLING-STATUS.adoc`](../TOOLING-STATUS.adoc). diff --git a/languages/wokelang.adoc b/languages/wokelang.adoc new file mode 100644 index 0000000..a28640d --- /dev/null +++ b/languages/wokelang.adoc @@ -0,0 +1,14 @@ +== WokeLang + +____ +No operation without explicit consent. +____ + +*Canonical repository:* +https://github.com/hyperpolymath/wokelang[hyperpolymath/wokelang] + +This coordinator only _indexes_ the language. The implementation, +specification, grammar, examples, and live status live in the canonical +repository above — not here. See also +link:../.machine_readable/LANGUAGES.a2ml[`+../.machine_readable/LANGUAGES.a2ml+`] +and link:../TOOLING-STATUS.adoc[`+../TOOLING-STATUS.adoc+`]. diff --git a/languages/wokelang.md b/languages/wokelang.md deleted file mode 100644 index eb6d7f5..0000000 --- a/languages/wokelang.md +++ /dev/null @@ -1,14 +0,0 @@ - -# WokeLang - -> No operation without explicit consent. - -**Canonical repository:** [hyperpolymath/wokelang](https://github.com/hyperpolymath/wokelang) - -This coordinator only *indexes* the language. The implementation, specification, grammar, -examples, and live status live in the canonical repository above — not here. See also -[`../.machine_readable/LANGUAGES.a2ml`](../.machine_readable/LANGUAGES.a2ml) and -[`../TOOLING-STATUS.adoc`](../TOOLING-STATUS.adoc). diff --git a/llm-warmup-dev.adoc b/llm-warmup-dev.adoc new file mode 100644 index 0000000..40a26a6 --- /dev/null +++ b/llm-warmup-dev.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — nextgen-languages (Developer) + +=== What is nextgen-languages? + +See README.adoc for overview. + +=== Key Commands + +* `+just setup+` — set up development environment +* `+just build+` — build the project +* `+just test+` — run tests +* `+just doctor+` — diagnose issues +* `+just heal+` — attempt auto-repair + +=== Quick Context + +* License: MPL-2.0 +* Part of hyperpolymath ecosystem +* See EXPLAINME.adoc for architecture diff --git a/llm-warmup-dev.md b/llm-warmup-dev.md deleted file mode 100644 index 89dc87f..0000000 --- a/llm-warmup-dev.md +++ /dev/null @@ -1,20 +0,0 @@ - -# LLM Warmup — nextgen-languages (Developer) - -## What is nextgen-languages? -See README.adoc for overview. - -## Key Commands -- `just setup` — set up development environment -- `just build` — build the project -- `just test` — run tests -- `just doctor` — diagnose issues -- `just heal` — attempt auto-repair - -## Quick Context -- License: MPL-2.0 -- Part of hyperpolymath ecosystem -- See EXPLAINME.adoc for architecture diff --git a/llm-warmup-user.adoc b/llm-warmup-user.adoc new file mode 100644 index 0000000..b06f3b0 --- /dev/null +++ b/llm-warmup-user.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — nextgen-languages (User) + +=== What is nextgen-languages? + +See README.adoc for overview. + +=== Key Commands + +* `+just setup+` — set up development environment +* `+just build+` — build the project +* `+just test+` — run tests +* `+just doctor+` — diagnose issues +* `+just heal+` — attempt auto-repair + +=== Quick Context + +* License: MPL-2.0 +* Part of hyperpolymath ecosystem +* See EXPLAINME.adoc for architecture diff --git a/llm-warmup-user.md b/llm-warmup-user.md deleted file mode 100644 index f1bd282..0000000 --- a/llm-warmup-user.md +++ /dev/null @@ -1,20 +0,0 @@ - -# LLM Warmup — nextgen-languages (User) - -## What is nextgen-languages? -See README.adoc for overview. - -## Key Commands -- `just setup` — set up development environment -- `just build` — build the project -- `just test` — run tests -- `just doctor` — diagnose issues -- `just heal` — attempt auto-repair - -## Quick Context -- License: MPL-2.0 -- Part of hyperpolymath ecosystem -- See EXPLAINME.adoc for architecture