From c9ceb33c9d772eefdaa8bda2e318e769651b8ed8 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 24 Aug 2026 08:23:35 +0100 Subject: [PATCH] refactor: migrate repository documentation from Markdown to AsciiDoc --- CHANGELOG.adoc | 9 + CHANGELOG.md | 11 - CODE_OF_CONDUCT.adoc | 24 ++ CODE_OF_CONDUCT.md | 27 --- CONTRIBUTING.adoc | 95 ++++++++ CONTRIBUTING.md | 78 ------- PROOF-NEEDS.adoc | 49 +++++ PROOF-NEEDS.md | 31 --- README.adoc | 386 +++++++++++++++++++++++++++++++++ README.md | 261 ---------------------- SECURITY.adoc | 16 ++ SECURITY.md | 20 -- TEST-NEEDS.adoc | 83 +++++++ TEST-NEEDS.md | 57 ----- TOPOLOGY.md => TOPOLOGY.adoc | 55 +++-- docs/tech-debt-2026-05-26.adoc | 80 +++++++ docs/tech-debt-2026-05-26.md | 71 ------ llm-warmup-dev.adoc | 19 ++ llm-warmup-dev.md | 16 -- llm-warmup-user.adoc | 19 ++ llm-warmup-user.md | 16 -- 21 files changed, 807 insertions(+), 616 deletions(-) create mode 100644 CHANGELOG.adoc delete mode 100644 CHANGELOG.md create mode 100644 CODE_OF_CONDUCT.adoc delete mode 100644 CODE_OF_CONDUCT.md create mode 100644 CONTRIBUTING.adoc delete mode 100644 CONTRIBUTING.md create mode 100644 PROOF-NEEDS.adoc delete mode 100644 PROOF-NEEDS.md create mode 100644 README.adoc delete mode 100644 README.md create mode 100644 SECURITY.adoc delete mode 100644 SECURITY.md create mode 100644 TEST-NEEDS.adoc delete mode 100644 TEST-NEEDS.md rename TOPOLOGY.md => TOPOLOGY.adoc (65%) create mode 100644 docs/tech-debt-2026-05-26.adoc delete mode 100644 docs/tech-debt-2026-05-26.md create mode 100644 llm-warmup-dev.adoc delete mode 100644 llm-warmup-dev.md create mode 100644 llm-warmup-user.adoc delete mode 100644 llm-warmup-user.md diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc new file mode 100644 index 0000000..ca1c652 --- /dev/null +++ b/CHANGELOG.adoc @@ -0,0 +1,9 @@ +== Changelog + +All notable changes to this project will be documented in this file. + +The format is based on https://keepachangelog.com/en/1.1.0/[Keep a +Changelog], and this project adheres to +https://semver.org/spec/v2.0.0.html[Semantic Versioning]. + +=== [Unreleased] diff --git a/CHANGELOG.md b/CHANGELOG.md deleted file mode 100644 index 8109476..0000000 --- a/CHANGELOG.md +++ /dev/null @@ -1,11 +0,0 @@ -# Changelog - -All notable changes to this project will be documented in this file. - -The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/), -and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). - - - - -## [Unreleased] 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 caeda1c..0000000 --- a/CODE_OF_CONDUCT.md +++ /dev/null @@ -1,27 +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..987d773 --- /dev/null +++ b/CONTRIBUTING.adoc @@ -0,0 +1,95 @@ +== Contributing + +Thank you for your interest in contributing! We follow a "`Dual-Track`" +architecture where human-readable documentation lives in the root and +machine-readable policies live in `+.machine_readable/+`. + +=== How to Contribute + +We welcome contributions in many forms: + +* *Code:* Improving the core stack or extensions +* *Documentation:* Enhancing docs or AI manifests +* *Testing:* Adding property-based tests or formal proofs +* *Bug reports:* Filing clear, reproducible issues + +=== Contribution model — Tri-Perimeter Contribution Framework (TPCF) + +kategoria follows the estate-wide *Tri-Perimeter Contribution Framework +(TPCF)* — graduated trust without gatekeeping: + +* *Perimeter 1 — Core Systems (maintainers only).* The proof kernel: the +level-indexed routes (`+routes/+`), the soundness/metatheory modules, +and the build/CI tooling. Direct commits by maintainers only (see +`+MAINTAINERS.adoc+`). +* *Perimeter 2 — Expert Extensions (trusted contributors).* New proof +routes, demos (`+examples/+`), and dependently-typed extensions. Apply +via issue → review → merge, with every Idris module type-checking under +`+idris2 --check+`. +* *Perimeter 3 — Community Sandbox (open to all).* Docs (`+.adoc+`), +`+.well-known/+` content, AI manifests, and spec proposals. + +==== Fork workflow + +External contributors use the standard *fork*-and-pull-request workflow: +fork the repository, branch from `+main+`, run `+just quality+` (and +`+idris2 --check+` on any touched proof module) locally, then open a PR. +Maintainers (Perimeter 1) may commit directly to feature branches. Proof +modules must type-check before review — a red Idris check blocks merge. + +=== Getting Started + +[arabic] +. *Read the AI Manifest:* Start with `+0-AI-MANIFEST.a2ml+` (if present) +to understand the repository structure. +. *Environment:* Use `+nix develop+` or `+direnv allow+` to set up your +tools. +. *Task Runner:* Use `+just+` to see available commands +(`+just --list+`). + +=== Development Workflow + +==== Branch Naming + +.... +docs/short-description # Documentation +test/what-added # Test additions +feat/short-description # New features +fix/issue-number-description # Bug fixes +refactor/what-changed # Code improvements +security/what-fixed # Security fixes +.... + +==== Commit Messages + +We follow https://www.conventionalcommits.org/[Conventional Commits]: + +.... +(): + +[optional body] + +[optional footer] +.... + +Types: `+feat+`, `+fix+`, `+docs+`, `+test+`, `+refactor+`, `+ci+`, +`+chore+`, `+security+` + +=== Reporting Bugs + +Before reporting: 1. Search existing issues 2. Check if it’s already +fixed in `+main+` + +When reporting, include: - Clear, descriptive title - Environment +details (OS, versions, toolchain) - Steps to reproduce - Expected vs +actual behaviour + +=== Code of Conduct + +All contributors are expected to adhere to our +link:CODE_OF_CONDUCT.md[Code of Conduct]. + +=== License + +By contributing, you agree that your contributions will be licensed +under the same license as the project (see LICENSE). diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md deleted file mode 100644 index b86cfd4..0000000 --- a/CONTRIBUTING.md +++ /dev/null @@ -1,78 +0,0 @@ - -# Contributing - -Thank you for your interest in contributing! We follow a "Dual-Track" architecture where human-readable documentation lives in the root and machine-readable policies live in `.machine_readable/`. - -## How to Contribute - -We welcome contributions in many forms: - -- **Code:** Improving the core stack or extensions -- **Documentation:** Enhancing docs or AI manifests -- **Testing:** Adding property-based tests or formal proofs -- **Bug reports:** Filing clear, reproducible issues - -## Contribution model — Tri-Perimeter Contribution Framework (TPCF) - -kategoria follows the estate-wide **Tri-Perimeter Contribution Framework (TPCF)** — graduated trust without gatekeeping: - -- **Perimeter 1 — Core Systems (maintainers only).** The proof kernel: the level-indexed routes (`routes/`), the soundness/metatheory modules, and the build/CI tooling. Direct commits by maintainers only (see `MAINTAINERS.adoc`). -- **Perimeter 2 — Expert Extensions (trusted contributors).** New proof routes, demos (`examples/`), and dependently-typed extensions. Apply via issue → review → merge, with every Idris module type-checking under `idris2 --check`. -- **Perimeter 3 — Community Sandbox (open to all).** Docs (`.adoc`), `.well-known/` content, AI manifests, and spec proposals. - -### Fork workflow - -External contributors use the standard **fork**-and-pull-request workflow: fork the repository, branch from `main`, run `just quality` (and `idris2 --check` on any touched proof module) locally, then open a PR. Maintainers (Perimeter 1) may commit directly to feature branches. Proof modules must type-check before review — a red Idris check blocks merge. - -## Getting Started - -1. **Read the AI Manifest:** Start with `0-AI-MANIFEST.a2ml` (if present) to understand the repository structure. -2. **Environment:** Use `nix develop` or `direnv allow` to set up your tools. -3. **Task Runner:** Use `just` to see available commands (`just --list`). - -## Development Workflow - -### Branch Naming - -``` -docs/short-description # Documentation -test/what-added # Test additions -feat/short-description # New features -fix/issue-number-description # Bug fixes -refactor/what-changed # Code improvements -security/what-fixed # Security fixes -``` - -### Commit Messages - -We follow [Conventional Commits](https://www.conventionalcommits.org/): - -``` -(): - -[optional body] - -[optional footer] -``` - -Types: `feat`, `fix`, `docs`, `test`, `refactor`, `ci`, `chore`, `security` - -## Reporting Bugs - -Before reporting: -1. Search existing issues -2. Check if it's already fixed in `main` - -When reporting, include: -- Clear, descriptive title -- Environment details (OS, versions, toolchain) -- Steps to reproduce -- Expected vs actual behaviour - -## Code of Conduct - -All contributors are expected to adhere to our [Code of Conduct](CODE_OF_CONDUCT.md). - -## License - -By contributing, you agree that your contributions will be licensed under the same license as the project (see [LICENSE](LICENSE)). diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc new file mode 100644 index 0000000..0c7dd8e --- /dev/null +++ b/PROOF-NEEDS.adoc @@ -0,0 +1,49 @@ +== PROOF-NEEDS.md — kategoria + +=== Current State + +* **src/abi/*.idr**: NO +* *Dangerous patterns*: 1 `+believe_me+` in `+Level09_SessionTypes.idr+` +(runtime placeholder for recv) +* *LOC*: ~4,400 (Idris2 routes + Nickel) +* *ABI layer*: Missing (but routes contain Idris2 type safety challenge +levels) + +=== What Needs Proving + +[width="100%",cols="51%,27%,22%",options="header",] +|=== +|Component |What |Why +|Session types (Level09) |Remove `+believe_me+` placeholder with real +recv implementation |Current believe_me bypasses type checker for +session receive + +|Cubical types (Level10) |Complete type equality proofs without +believe_me |Level10 notes need for believe_me; should use proper cubical +path types + +|Route completeness |All 5 routes (alpha-epsilon) have total, proven +implementations |Challenge levels should themselves be provably correct + +|K9 contractile guards |believe_me/assert_total ceiling enforcement is +sound |Meta-level: the guards themselves need correctness proofs +|=== + +=== Recommended Prover + +*Idris2* — The repo IS an Idris2 type safety challenge. The believe_me +in Level09 is the primary proof gap. Level10 cubical types may benefit +from *Agda* with cubical support. + +=== Priority + +*MEDIUM* — Educational/challenge repo, but the believe_me in Level09 +undermines the repo’s own thesis. Fixing it would demonstrate the very +point the challenge makes. + +=== Template ABI Cleanup (2026-03-29) + +Template ABI removed – was creating false impression of formal +verification. The removed files (Types.idr, Layout.idr, Foreign.idr) +contained only RSR template scaffolding with unresolved +\{\{PROJECT}}/\{\{AUTHOR}} placeholders and no domain-specific proofs. diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md deleted file mode 100644 index df70c96..0000000 --- a/PROOF-NEEDS.md +++ /dev/null @@ -1,31 +0,0 @@ -# PROOF-NEEDS.md — kategoria - -## Current State - -- **src/abi/*.idr**: NO -- **Dangerous patterns**: 1 `believe_me` in `Level09_SessionTypes.idr` (runtime placeholder for recv) -- **LOC**: ~4,400 (Idris2 routes + Nickel) -- **ABI layer**: Missing (but routes contain Idris2 type safety challenge levels) - -## What Needs Proving - -| Component | What | Why | -|-----------|------|-----| -| Session types (Level09) | Remove `believe_me` placeholder with real recv implementation | Current believe_me bypasses type checker for session receive | -| Cubical types (Level10) | Complete type equality proofs without believe_me | Level10 notes need for believe_me; should use proper cubical path types | -| Route completeness | All 5 routes (alpha-epsilon) have total, proven implementations | Challenge levels should themselves be provably correct | -| K9 contractile guards | believe_me/assert_total ceiling enforcement is sound | Meta-level: the guards themselves need correctness proofs | - -## Recommended Prover - -**Idris2** — The repo IS an Idris2 type safety challenge. The believe_me in Level09 is the primary proof gap. Level10 cubical types may benefit from **Agda** with cubical support. - -## Priority - -**MEDIUM** — Educational/challenge repo, but the believe_me in Level09 undermines the repo's own thesis. Fixing it would demonstrate the very point the challenge makes. - -## Template ABI Cleanup (2026-03-29) - -Template ABI removed -- was creating false impression of formal verification. -The removed files (Types.idr, Layout.idr, Foreign.idr) contained only RSR template -scaffolding with unresolved {{PROJECT}}/{{AUTHOR}} placeholders and no domain-specific proofs. diff --git a/README.adoc b/README.adoc new file mode 100644 index 0000000..7aeb36a --- /dev/null +++ b/README.adoc @@ -0,0 +1,386 @@ +// SPDX-License-Identifier: MPL-2.0 = Kategoria — The Type Safety +Challenge :toc: preamble :toc-title: Contents :icons: font :doctype: +article + +Five approaches to building a language with every known level of type +safety. Named after Aristotle’s Κατηγορίαι. + +== Overview + +As of 2026, type theory has identified 10 distinct levels of type +safety. No single production language covers all 10. Most cover 3–4. The +best (Idris 2) covers 7. + +Kategoria is an exploration, not a product. We try five routes toward +full coverage, share what we learn, and document everything—including +the failures. The stumble journal is the most important artefact. + +Why this exists: type theory is the invisible engineering behind every +compiler error that prevents a bug. Most working programmers have never +heard the term. Most PL courses stop at level 3. This project maps the +territory from level 1 to level 10 and beyond. + +== The 10 known levels (as of 2026) + +[cols="`1,2,2,2`", options="`header`"] |=== | Level | What it catches | +Example | First appeared + +[verse] +-- +1. Basic Types +Mixing incompatible primitives +`+1 + "hello"+` rejected +FORTRAN (1957) +-- + +[verse] +-- +2. Algebraic Data Types +Missing cases, impossible states +`+Option+` forces handling `+None+` +ML (1973) +-- + +[verse] +-- +3. Parametric Polymorphism +Accidental type assumptions in generic code +`+id(x: T) → T+` cannot inspect `+T+` +System F (1972) +-- + +[verse] +-- +4. Higher-Kinded Types +Incompatible abstractions +`+List+` and `+Option+` are both `+Functor+` +Haskell (1990) +-- + +[verse] +-- +5. GADTs +Ill-typed expressions in DSLs +`+Expr+` vs `+Expr+` tracked by the type system +GHC (~2005) +-- + +[verse] +-- +6. Dependent Types +Logical errors provable at compile time +`+Vec 3 Int+`; `+head+` on empty is a type error +LF (1986), Coq, Agda, Idris +-- + +[verse] +-- +7. Linear / Affine Types +Resource leaks, double-free, use-after-close +File handle closed exactly once +Linear Logic (1987), Rust, Idris 2 +-- + +[verse] +-- +8. Refinement Types +Violated preconditions +`+{x : Int \| x > 0}+`; division by zero is a type error +LF/SMT (2000s), F*, Liquid Haskell +-- + +[verse] +-- +9. Session Types +Protocol violations in communication +Send Int, receive Bool, close; out-of-order is a type error +Honda (1993) +-- + +[verse] +-- +10. Homotopy / Cubical Types +Unsound type equivalences +`+Bool ≃ Bool+` has exactly two valid equivalences +HoTT (2013), cubicaltt, Agda –cubical +-- + +|=== + +The correspondence to Aristotle’s 10 categories is a motivating +observation, not a theorem. It may be coincidence, deep structure, or an +artifact of how we count. We track it because it suggests the list may +not be complete. + +== The five routes + +We do not know which approach will work. We try five, share results, and +document failures. + +All routes share a common test suite (10 challenge programs, one per +level) and interface type specification. + +[cols="`1,2,3,2`", options="`header`"] |=== | Route | Strategy | Key +question | Levels native + +[verse] +-- +α (Alpha): Extend Idris 2 +Start from the strongest existing foundation; push upward via elaborator reflection and plugins +How far can you extend a language before you need to replace its core? +1–7 native; 8–9 via encoding +-- + +[verse] +-- +β (Beta): Dyadic Split +Two languages sharing syntax/parser, diverging at the type checker (QTT core + Cubical core) +Can two type checkers share enough to feel like one language? +β-1: 1–8; β-2: 8–10 +-- + +[verse] +-- +γ (Gamma): Aspect Injection +Stable dependent+QTT core; weave independent type-checking aspects at defined compilation points +Can independent type checkers compose when a single proof needs guarantees from multiple levels? +Core: 1–7; Aspects: 8, 9, 10 +-- + +[verse] +-- +δ (Delta): Aggregate Bridge +Use existing best-in-class languages per level range; bridge through shared ABI/FFI +Can type safety survive crossing a language boundary? +Idris 2 (1–7), F* (8), Scribble (9), Agda –cubical (10) +-- + +[verse] +-- +ε (Epsilon): Clean Slate +New core calculus unifying everything; no legacy constraints +Is there a consistent type theory that subsumes all 10 levels, or is the fragmentation fundamental? +All (if it exists) +-- + +|=== + +== Progress + +[cols="`1,1,1,1,1,1,1,1,1,1,1`", options="`header`"] |=== | Route | L1 | +L2 | L3 | L4 | L5 | L6 | L7 | L8 | L9 | L10 + +[verse] +-- +α Extend +✓ | ✓ | ✓ | ✓ | ✓ | ✓ | ✓ | ✓~ | ✓~ | ✗ +-- + +[verse] +-- +β Dyadic +. | . | . | . | . | . | . | . | . | . +-- + +[verse] +-- +γ Aspect +. | . | . | . | . | . | . | . | . | . +-- + +[verse] +-- +δ Aggregate +. | . | . | . | . | . | . | . | . | . +-- + +[verse] +-- +ε Clean +. | . | . | . | . | . | . | . | . | . +-- + +|=== + +_✓ = passing, ✓~ = passing via encoding, . = not started, ✗ = proven +impossible on this route_ + +Route α is enforced by CI (`+scripts/check-idris2-proofs.sh+`). L8 and +L9 pass via encodings (dependent pairs for refinement; Brady’s indexed +monad for sessions), not native type formers. L10 is route α’s +documented wall (QTT and cubical type theory are different foundations). + +Route δ has a measurement bridge (Typell) mapped level-by-level, but no +running implementation yet. + +== TypeFix Zero (TF0) + +A standalone calibration calculus. Where Kategoria explores routes +toward high-assurance type safety, TF0 strips down to the smallest +typed, Turing-complete core that remains mathematically honest: universe +stratification, function types, naturals, lambda, and one explicit +fixed-point primitive. + +TF0 is a diagnostic tool for testing claims about universe hierarchies, +the total/partial boundary, and the minimum machinery for +Turing-completeness. It is not a Katoria implementation target. + +== Level 11 and beyond + +== [CAUTION] + +== State of the art as of 2026. Type theory is not finished. If you know of a level we have missed, open an issue. We would rather discover we were wrong than remain confidently incomplete. + +Active research areas that may constitute future levels: + +[cols="`1,2,2`", options="`header`"] |=== | Candidate | What it would +add | Maturity + +[verse] +-- +Graded types +Semiring-indexed resource tracking (generalises linear) +Working compiler (Granule) +-- + +[verse] +-- +Effect types +Side effects tracked and controlled in the type system +Production-ready (Koka) +-- + +[verse] +-- +Modal types +Necessity, possibility, temporality as type operators +30+ years of theory, limited implementations +-- + +[verse] +-- +Directed types +Types as categories, morphisms as programs +Very early (2023 preprints) +-- + +[verse] +-- +Capability types +Authority-based access control in the type system +Proven in Pony, language inactive +-- + +[verse] +-- +Observational equality +Alternative foundation for equality (not cubical) +May replace Level 10 rather than extend it +-- + +[verse] +-- +Sized types +Termination guaranteed by structural size +Stable in Agda +-- + +[verse] +-- +Gradual types +Sound mixing of static and dynamic typing +Mature theory, production use +-- + +|=== + +== What is standard and what is ours + +[cols="`1,2,2`", options="`header`"] |=== | Concept | Status | Home + +[verse] +-- +The 10 levels of type safety +Standard (assembled from existing literature) +The framing is ours +-- + +[verse] +-- +Route α (extend Idris 2) +Standard engineering strategy +The specific encodings and L10 wall are ours +-- + +[verse] +-- +Routes β–ε +*Novel assembly strategies* +The routes themselves +-- + +[verse] +-- +TF0 +Standard minimal calculus construction +The calibration application is ours +-- + +[verse] +-- +Stumble journal +*Novel methodology* (shared with echo-types retraction ledger) +The journal +-- + +|=== + +== How to participate + +* *Type theorists:* Tell us when we are wrong. If a route makes an +unsound assumption or reinvents something solved in 1988, open an issue. +* *Language developers:* Pick a route. Build. Document decisions in +`+docs/+`. +* *Curious readers:* Read the stumble journal. Watching five approaches +hit five different walls teaches more than any textbook. + +There is no winner. The point is to map the territory. + +== Documentation + +* link:EXPLAINME.adoc[EXPLAINME] — claim-by-claim receipts and known +gaps +* link:Glossary.adoc[Glossary] — terminology reference +* `+docs/stumble-journal/+` — what went wrong, why, and what we learned +* `+docs/shine-journal/+` — what worked unexpectedly well +* `+docs/cross-pollination/+` — discoveries from one route that helped +another +* `+docs/methodology/+` — constraint-first development, LLM +collaboration field reports + +== Build + +=== [source,bash] + +== Route α (Idris 2) + +cd routes/alpha-extend/ idris2 –build Alpha.ipkg + +== CI check (rejects axiom smuggling) + +=== scripts/check-idris2-proofs.sh + +== License + +SPDX-License-Identifier: MPL-2.0 — see link:LICENSE[LICENSE].| Mature +theory, production use |=== + +== What is standard and what is ours + +[cols="`1,2,2`", options="`header`"] |=== | Concept | Status | Home + +[verse] +-- +The 10 levels of type safety +Standard (assembled from existing literature) +-- diff --git a/README.md b/README.md deleted file mode 100644 index bc718bd..0000000 --- a/README.md +++ /dev/null @@ -1,261 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -= Kategoria — The Type Safety Challenge -:toc: preamble -:toc-title: Contents -:icons: font -:doctype: article - -Five approaches to building a language with every known level of type safety. Named after Aristotle's Κατηγορίαι. - -== Overview - -As of 2026, type theory has identified 10 distinct levels of type safety. No single production language covers all 10. Most cover 3–4. The best (Idris 2) covers 7. - -Kategoria is an exploration, not a product. We try five routes toward full coverage, share what we learn, and document everything—including the failures. The stumble journal is the most important artefact. - -Why this exists: type theory is the invisible engineering behind every compiler error that prevents a bug. Most working programmers have never heard the term. Most PL courses stop at level 3. This project maps the territory from level 1 to level 10 and beyond. - -== The 10 known levels (as of 2026) - -[cols="1,2,2,2", options="header"] -|=== -| Level | What it catches | Example | First appeared - -| 1. Basic Types -| Mixing incompatible primitives -| `1 + "hello"` rejected -| FORTRAN (1957) - -| 2. Algebraic Data Types -| Missing cases, impossible states -| `Option` forces handling `None` -| ML (1973) - -| 3. Parametric Polymorphism -| Accidental type assumptions in generic code -| `id(x: T) → T` cannot inspect `T` -| System F (1972) - -| 4. Higher-Kinded Types -| Incompatible abstractions -| `List` and `Option` are both `Functor` -| Haskell (1990) - -| 5. GADTs -| Ill-typed expressions in DSLs -| `Expr` vs `Expr` tracked by the type system -| GHC (~2005) - -| 6. Dependent Types -| Logical errors provable at compile time -| `Vec 3 Int`; `head` on empty is a type error -| LF (1986), Coq, Agda, Idris - -| 7. Linear / Affine Types -| Resource leaks, double-free, use-after-close -| File handle closed exactly once -| Linear Logic (1987), Rust, Idris 2 - -| 8. Refinement Types -| Violated preconditions -| `{x : Int \| x > 0}`; division by zero is a type error -| LF/SMT (2000s), F*, Liquid Haskell - -| 9. Session Types -| Protocol violations in communication -| Send Int, receive Bool, close; out-of-order is a type error -| Honda (1993) - -| 10. Homotopy / Cubical Types -| Unsound type equivalences -| `Bool ≃ Bool` has exactly two valid equivalences -| HoTT (2013), cubicaltt, Agda --cubical -|=== - -The correspondence to Aristotle's 10 categories is a motivating observation, not a theorem. It may be coincidence, deep structure, or an artifact of how we count. We track it because it suggests the list may not be complete. - -== The five routes - -We do not know which approach will work. We try five, share results, and document failures. - -All routes share a common test suite (10 challenge programs, one per level) and interface type specification. - -[cols="1,2,3,2", options="header"] -|=== -| Route | Strategy | Key question | Levels native - -| α (Alpha): Extend Idris 2 -| Start from the strongest existing foundation; push upward via elaborator reflection and plugins -| How far can you extend a language before you need to replace its core? -| 1–7 native; 8–9 via encoding - -| β (Beta): Dyadic Split -| Two languages sharing syntax/parser, diverging at the type checker (QTT core + Cubical core) -| Can two type checkers share enough to feel like one language? -| β-1: 1–8; β-2: 8–10 - -| γ (Gamma): Aspect Injection -| Stable dependent+QTT core; weave independent type-checking aspects at defined compilation points -| Can independent type checkers compose when a single proof needs guarantees from multiple levels? -| Core: 1–7; Aspects: 8, 9, 10 - -| δ (Delta): Aggregate Bridge -| Use existing best-in-class languages per level range; bridge through shared ABI/FFI -| Can type safety survive crossing a language boundary? -| Idris 2 (1–7), F* (8), Scribble (9), Agda --cubical (10) - -| ε (Epsilon): Clean Slate -| New core calculus unifying everything; no legacy constraints -| Is there a consistent type theory that subsumes all 10 levels, or is the fragmentation fundamental? -| All (if it exists) -|=== - -== Progress - -[cols="1,1,1,1,1,1,1,1,1,1,1", options="header"] -|=== -| Route | L1 | L2 | L3 | L4 | L5 | L6 | L7 | L8 | L9 | L10 - -| α Extend -| ✓ | ✓ | ✓ | ✓ | ✓ | ✓ | ✓ | ✓~ | ✓~ | ✗ - -| β Dyadic -| . | . | . | . | . | . | . | . | . | . - -| γ Aspect -| . | . | . | . | . | . | . | . | . | . - -| δ Aggregate -| . | . | . | . | . | . | . | . | . | . - -| ε Clean -| . | . | . | . | . | . | . | . | . | . -|=== - -*✓ = passing, ✓~ = passing via encoding, . = not started, ✗ = proven impossible on this route* - -Route α is enforced by CI (`scripts/check-idris2-proofs.sh`). L8 and L9 pass via encodings (dependent pairs for refinement; Brady's indexed monad for sessions), not native type formers. L10 is route α's documented wall (QTT and cubical type theory are different foundations). - -Route δ has a measurement bridge (Typell) mapped level-by-level, but no running implementation yet. - -== TypeFix Zero (TF0) - -A standalone calibration calculus. Where Kategoria explores routes toward high-assurance type safety, TF0 strips down to the smallest typed, Turing-complete core that remains mathematically honest: universe stratification, function types, naturals, lambda, and one explicit fixed-point primitive. - -TF0 is a diagnostic tool for testing claims about universe hierarchies, the total/partial boundary, and the minimum machinery for Turing-completeness. It is not a Katoria implementation target. - -== Level 11 and beyond - -[CAUTION] -==== -State of the art as of 2026. Type theory is not finished. If you know of a level we have missed, open an issue. We would rather discover we were wrong than remain confidently incomplete. -==== - -Active research areas that may constitute future levels: - -[cols="1,2,2", options="header"] -|=== -| Candidate | What it would add | Maturity - -| Graded types -| Semiring-indexed resource tracking (generalises linear) -| Working compiler (Granule) - -| Effect types -| Side effects tracked and controlled in the type system -| Production-ready (Koka) - -| Modal types -| Necessity, possibility, temporality as type operators -| 30+ years of theory, limited implementations - -| Directed types -| Types as categories, morphisms as programs -| Very early (2023 preprints) - -| Capability types -| Authority-based access control in the type system -| Proven in Pony, language inactive - -| Observational equality -| Alternative foundation for equality (not cubical) -| May replace Level 10 rather than extend it - -| Sized types -| Termination guaranteed by structural size -| Stable in Agda - -| Gradual types -| Sound mixing of static and dynamic typing -| Mature theory, production use -|=== - -== What is standard and what is ours - -[cols="1,2,2", options="header"] -|=== -| Concept | Status | Home - -| The 10 levels of type safety -| Standard (assembled from existing literature) -| The framing is ours - -| Route α (extend Idris 2) -| Standard engineering strategy -| The specific encodings and L10 wall are ours - -| Routes β–ε -| **Novel assembly strategies** -| The routes themselves - -| TF0 -| Standard minimal calculus construction -| The calibration application is ours - -| Stumble journal -| **Novel methodology** (shared with echo-types retraction ledger) -| The journal -|=== - -== How to participate - -* **Type theorists:** Tell us when we are wrong. If a route makes an unsound assumption or reinvents something solved in 1988, open an issue. -* **Language developers:** Pick a route. Build. Document decisions in `docs/`. -* **Curious readers:** Read the stumble journal. Watching five approaches hit five different walls teaches more than any textbook. - -There is no winner. The point is to map the territory. - -== Documentation - -* link:EXPLAINME.adoc[EXPLAINME] — claim-by-claim receipts and known gaps -* link:Glossary.adoc[Glossary] — terminology reference -* `docs/stumble-journal/` — what went wrong, why, and what we learned -* `docs/shine-journal/` — what worked unexpectedly well -* `docs/cross-pollination/` — discoveries from one route that helped another -* `docs/methodology/` — constraint-first development, LLM collaboration field reports - -== Build - -[source,bash] ----- -# Route α (Idris 2) -cd routes/alpha-extend/ -idris2 --build Alpha.ipkg - -# CI check (rejects axiom smuggling) -scripts/check-idris2-proofs.sh ----- - -== License - -SPDX-License-Identifier: MPL-2.0 — see link:LICENSE[LICENSE].| Mature theory, production use -|=== - -== What is standard and what is ours - -[cols="1,2,2", options="header"] -|=== -| Concept | Status | Home - -| The 10 levels of type safety -| Standard (assembled from existing literature) diff --git a/SECURITY.adoc b/SECURITY.adoc new file mode 100644 index 0000000..e47fdd9 --- /dev/null +++ b/SECURITY.adoc @@ -0,0 +1,16 @@ +== Security Policy + +=== Reporting a Vulnerability + +If you discover a security vulnerability, please report it responsibly. + +*Email:* j.d.a.jewell@open.ac.uk + +*Please include:* - Description of the vulnerability - Steps to +reproduce - Potential impact + +*Response timeline:* - Acknowledgement within 48 hours - Initial +assessment within 7 days - Fix or mitigation within 90 days + +*Safe harbour:* We will not pursue legal action against security +researchers who follow responsible disclosure. diff --git a/SECURITY.md b/SECURITY.md deleted file mode 100644 index 5c4d5e9..0000000 --- a/SECURITY.md +++ /dev/null @@ -1,20 +0,0 @@ - -# Security Policy - -## Reporting a Vulnerability - -If you discover a security vulnerability, please report it responsibly. - -**Email:** j.d.a.jewell@open.ac.uk - -**Please include:** -- Description of the vulnerability -- Steps to reproduce -- Potential impact - -**Response timeline:** -- Acknowledgement within 48 hours -- Initial assessment within 7 days -- Fix or mitigation within 90 days - -**Safe harbour:** We will not pursue legal action against security researchers who follow responsible disclosure. diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc new file mode 100644 index 0000000..77b0461 --- /dev/null +++ b/TEST-NEEDS.adoc @@ -0,0 +1,83 @@ +== TEST-NEEDS.md — kategoria + +=== CRG Grade: C — ACHIEVED 2026-04-04 + +____ +Generated 2026-03-29 by punishing audit. +____ + +=== Current State + +[cols=",,",options="header",] +|=== +|Category |Count |Notes +|Unit tests |0 |None +|Integration |1 |Zig FFI integration_test.zig +|E2E |0 |None +|Benchmarks |0 |None +|=== + +*Source modules:* 3 Idris2 ABI (Types, Layout, Foreign), 1 Zig FFI, 10 +Idris2 route levels (Level01-Level10), 3 example demos, 1 ReScript +example. ~16 Idris2 files total, 3 Zig files. + +=== What’s Missing + +==== P2P (Property-Based) Tests + +* [ ] Type level route completeness: property tests that each level’s +types are well-formed +* [ ] ABI layout: property tests for struct alignment and size +invariants +* [ ] FFI roundtrip: property tests for Idris2->Zig->Idris2 data +integrity + +==== E2E Tests + +* [ ] Full 10-level type progression: Level01 through Level10 +compilation and verification +* [ ] Example execution: each demo (ProvenArithmetic, SafeAPI, +StateMachine) runs to completion +* [ ] ABI/FFI round-trip: Idris2 definition -> C header -> Zig +implementation -> verification + +==== Aspect Tests + +* *Security:* No tests for type safety guarantees (the entire point of +the project) +* *Performance:* No compilation time benchmarks for dependent type +checking +* *Concurrency:* N/A for this project +* *Error handling:* No tests for malformed type definitions, invalid +level progressions + +==== Build & Execution + +* [ ] Idris2 compilation of all .idr files +* [ ] Zig build + test execution +* [ ] Example compilation verification + +==== Benchmarks Needed + +* [ ] Type checking time per level (Level01-Level10) +* [ ] FFI call overhead measurement + +==== Self-Tests + +* [ ] Type level proof verification (each level’s proofs type-check) +* [ ] ABI version agreement between Idris2 and Zig + +=== Priority + +*HIGH.* A type theory teaching tool with ZERO unit tests for 10 type +levels is embarrassing. The single FFI integration test is not enough. +Each of the 10 levels should have its own test suite proving the +type-level guarantees actually hold. + +=== 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 e9489e7..0000000 --- a/TEST-NEEDS.md +++ /dev/null @@ -1,57 +0,0 @@ -# TEST-NEEDS.md — kategoria - -## CRG Grade: C — ACHIEVED 2026-04-04 - -> Generated 2026-03-29 by punishing audit. - -## Current State - -| Category | Count | Notes | -|-------------|-------|-------| -| Unit tests | 0 | None | -| Integration | 1 | Zig FFI integration_test.zig | -| E2E | 0 | None | -| Benchmarks | 0 | None | - -**Source modules:** 3 Idris2 ABI (Types, Layout, Foreign), 1 Zig FFI, 10 Idris2 route levels (Level01-Level10), 3 example demos, 1 ReScript example. ~16 Idris2 files total, 3 Zig files. - -## What's Missing - -### P2P (Property-Based) Tests -- [ ] Type level route completeness: property tests that each level's types are well-formed -- [ ] ABI layout: property tests for struct alignment and size invariants -- [ ] FFI roundtrip: property tests for Idris2->Zig->Idris2 data integrity - -### E2E Tests -- [ ] Full 10-level type progression: Level01 through Level10 compilation and verification -- [ ] Example execution: each demo (ProvenArithmetic, SafeAPI, StateMachine) runs to completion -- [ ] ABI/FFI round-trip: Idris2 definition -> C header -> Zig implementation -> verification - -### Aspect Tests -- **Security:** No tests for type safety guarantees (the entire point of the project) -- **Performance:** No compilation time benchmarks for dependent type checking -- **Concurrency:** N/A for this project -- **Error handling:** No tests for malformed type definitions, invalid level progressions - -### Build & Execution -- [ ] Idris2 compilation of all .idr files -- [ ] Zig build + test execution -- [ ] Example compilation verification - -### Benchmarks Needed -- [ ] Type checking time per level (Level01-Level10) -- [ ] FFI call overhead measurement - -### Self-Tests -- [ ] Type level proof verification (each level's proofs type-check) -- [ ] ABI version agreement between Idris2 and Zig - -## Priority - -**HIGH.** A type theory teaching tool with ZERO unit tests for 10 type levels is embarrassing. The single FFI integration test is not enough. Each of the 10 levels should have its own test suite proving the type-level guarantees actually hold. - -## 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 65% rename from TOPOLOGY.md rename to TOPOLOGY.adoc index d566ae2..cce831d 100644 --- a/TOPOLOGY.md +++ b/TOPOLOGY.adoc @@ -1,19 +1,16 @@ - - +== TOPOLOGY.md — kategoria -# TOPOLOGY.md — kategoria +=== Purpose -## Purpose +Kategoria: The Type Safety Challenge. Five independent +language-implementation routes exploring all 10 known levels of type +safety. Named after Aristotle’s _Categories_ (c. 350 BCE); explores the +deep relationship between ancient philosophy and modern type theory +across 10 levels of safety that no single production language covers. -Kategoria: The Type Safety Challenge. Five independent language-implementation -routes exploring all 10 known levels of type safety. Named after Aristotle's -*Categories* (c. 350 BCE); explores the deep relationship between ancient -philosophy and modern type theory across 10 levels of safety that no single -production language covers. +=== Module Map -## Module Map - -``` +.... kategoria/ ├── routes/ │ └── alpha-extend/ # Route α: Extend Idris 2 (the only route with code) @@ -42,30 +39,32 @@ kategoria/ ├── ROADMAP.adoc # Route-by-route progress ├── README.md # Challenge definition, the five routes, scorecard └── LICENSE # MPL-2.0 (code); CC-BY-SA-4.0 (docs) -``` +.... -The `approach-1/ … approach-5/` and `spec/` directories described by earlier -revisions of this file never existed in this repository; the map above is the -measured layout (2026-07-21). +The `+approach-1/ … approach-5/+` and `+spec/+` directories described by +earlier revisions of this file never existed in this repository; the map +above is the measured layout (2026-07-21). -## Data Flow +=== Data Flow -``` +.... [Aristotle's 10 Categories] ──► [Type Theory Parallels] ──► [5 Routes to Implementation] ↓ [Compare Coverage & Soundness] ↓ [Feed: typell verification kernel (routes/delta-aggregate/TYPELL-BRIDGE.adoc)] -``` +.... -## Key Invariants +=== Key Invariants -- Five independent routes avoid lock-in to a single design -- Each route documents which type-safety levels it covers — and which it - provably cannot (route α's L10 wall is recorded, not hidden) -- Every claimed proof is enforced by `scripts/check-idris2-proofs.sh`: - no postulates, no believe_me, no %hint smuggling, no skipping when the - prover is missing -- Philosophy: explore the type-space rather than build one production language -- Aristotelian framing: systematic classification of fundamental concepts +* Five independent routes avoid lock-in to a single design +* Each route documents which type-safety levels it covers — and which it +provably cannot (route α’s L10 wall is recorded, not hidden) +* Every claimed proof is enforced by `+scripts/check-idris2-proofs.sh+`: +no postulates, no believe_me, no %hint smuggling, no skipping when the +prover is missing +* Philosophy: explore the type-space rather than build one production +language +* Aristotelian framing: systematic classification of fundamental +concepts diff --git a/docs/tech-debt-2026-05-26.adoc b/docs/tech-debt-2026-05-26.adoc new file mode 100644 index 0000000..71c2be8 --- /dev/null +++ b/docs/tech-debt-2026-05-26.adoc @@ -0,0 +1,80 @@ +== Tech-Debt Audit — kategoria — 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= 13 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 1 | 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 |352 +|`+docs/+` files |61 +|`+docs/+` LoC |2694 +|CHANGELOG.md |Y +|CONTRIBUTING.md |Y +|CODE_OF_CONDUCT.md |Y +|SECURITY.md |Y +|Severity |`+OK+` +|=== + +*Recommended next move:* none for docs. + +=== 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 9b626b8..0000000 --- a/docs/tech-debt-2026-05-26.md +++ /dev/null @@ -1,71 +0,0 @@ - - -# Tech-Debt Audit — kategoria — 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= 13 | Coq-Axm/Adm= 0 | Lean-srry/ax= 0 | Agda-pst= 0 | Idr-blv= 1 | 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 | 352 | -| `docs/` files | 61 | -| `docs/` LoC | 2694 | -| CHANGELOG.md | Y | -| CONTRIBUTING.md | Y | -| CODE_OF_CONDUCT.md | Y | -| SECURITY.md | Y | -| Severity | `OK` | - -**Recommended next move:** none for docs. - -## 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/llm-warmup-dev.adoc b/llm-warmup-dev.adoc new file mode 100644 index 0000000..9a4a77e --- /dev/null +++ b/llm-warmup-dev.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — kategoria (Developer) + +=== What is kategoria? + +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 fde115e..0000000 --- a/llm-warmup-dev.md +++ /dev/null @@ -1,16 +0,0 @@ -# LLM Warmup — kategoria (Developer) - -## What is kategoria? -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..a111dea --- /dev/null +++ b/llm-warmup-user.adoc @@ -0,0 +1,19 @@ +== LLM Warmup — kategoria (User) + +=== What is kategoria? + +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 561a9c7..0000000 --- a/llm-warmup-user.md +++ /dev/null @@ -1,16 +0,0 @@ -# LLM Warmup — kategoria (User) - -## What is kategoria? -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