diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc new file mode 100644 index 0000000..8e6c9a4 --- /dev/null +++ b/AFFIRMATION.adoc @@ -0,0 +1,138 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell += WokeLang — Affirmation of Current State +:toc: +:sectnums: +:affirmed: 2026-06-19 +:revdate: 2026-06-19 + +[abstract] +A point-in-time *affirmation* of where WokeLang stands: a timestamped +attestation of what is true now, organised as the project's normative +*MUST / INTEND / WISH* standing. It is a report, not a gate — the hard gates +live in `.machine_readable/contractiles/` (the `must` contractile). + +[NOTE] +==== +*Provenance & method.* Produced in an AI-assisted (Claude Code) working +session, reflecting the state after the proof and bytecode-VM work merged on +2026-06-18/19 (PRs #90–#94). It follows the RSR conventions visible in this +repository; the canonical `AFFIRMATION.adoc` template in +`hyperpolymath/standards` was *not reachable from this session*, so reconcile +this document against that template when available. +==== + +== Affirmation + +As of *{affirmed}*, we affirm that WokeLang is a *working, consent-driven, +human-centred programming language* whose *type safety is machine-checked and +CI-gated* for a deliberately-scoped expression/statement core. Its normative +MUSTs hold. The live development frontier is making the bytecode VM a true +second compilation target and reconciling documentation to reality. + +== MUST — the normative core (what WokeLang must be to *be* itself) + +[cols="3,1,4",options="header"] +|=== +| MUST | Status | Where we are + +| A working language: lex → parse → typecheck → run `.woke` +| ✅ met +| Rust toolchain (parser, typechecker, interpreter, bytecode VM, LSP, DAP, formatter, linter, REPL); 188 lib tests; OCaml reference core + +| Consent-driven safety actually *enforced* (the defining feature) +| ✅ met +| Interpreter always; the *VM now enforces* under `#care` (deny-by-default, PR #92); consent lives in the type system of the Idris calculus + +| Machine-checked type safety (progress + preservation) +| ✅ met (core) +| Lean + Coq (expression core + arrays + statement typing) and the Idris consent calculus. A *deliberate subset* of the surface language + +| Proofs sound and non-rotting (CI-gated, `sorry`/axiom-free) +| ✅ met +| `lean-proofs.yml` + `coq-proofs.yml`; axiom-free bar Coq's unavoidable reals axioms + +| Human-centred + ethical scaffolding (consent, gratitude, emotes, Result) +| ✅ met +| In the interpreter and now the VM + +| RSR repository compliance (license/governance/contractiles) +| ✅ mostly +| Template `Mustfile` checks pass; commit-signing `must` is the soft spot +|=== + +== INTEND — committed next-actions (we WILL do this) + +[cols="3,1,4",options="header"] +|=== +| INTENT | Status | Where we are + +| Make the bytecode VM a real compilation target +| in_progress +| Major strides 2026-06-18/19: machine opcodes, full expr/stmt coverage, consent enforcement, Result constructors, closures + upvalue capture. Remainder → wishes + +| Broaden the verified core toward the Rust type system +| in_progress +| binop parity + arrays + statement typing landed; float arithmetic still open + +| Reconcile documentation to reality +| declared +| README/EXPLAINME stale; `TOOLCHAIN-WISHLIST` lists *built* tools (LSP/DAP/WASM) as "missing"; completion figure contradicts (`STATE.a2ml` 35% vs wishlist 85%) + +| Integrate echo-types into the type checker +| declared +| `STATE.a2ml` frontier; not started + +| Resolve eval ↔ spec correspondence (PROOF-NEEDS #2) +| declared +| Needs a maintainer decision (treat the spec as normative, or build a second model) +|=== + +== WISH — horizon aspirations (we WISH this were true) + +[cols="4,1,1",options="header"] +|=== +| WISH | Horizon | Status + +| Interpreter↔VM parity harness (conformance through both) | near | declared +| `.wbc` bytecode serialization | near | declared +| Consent grant-sources (`superpower` declarations) on the VM | near | declared +| Worker / concurrency statements on the VM | near | declared +| By-reference + multi-level closure capture | near | declared +| Full surface-language type safety (statement dynamics, units, pattern matching) | mid | declared +| WASM codegen correctness | mid | declared +| Remaining dev tooling (debugger UI, profiler, package manager, doc-gen) | mid | declared +| Ordinal/echo Bachmann–Howard consumer-evidence; formal VM↔spec compiler-correctness | far | declared +| Establishment (paper / Zenodo) + production-grade toolchain | far | declared +|=== + +== Where we are (synthesis) + +WokeLang's MUSTs are met for a deliberately-scoped core: a real, running, +consent-enforcing language whose type safety is machine-checked and CI-gated. +The frontier is the INTEND layer — turning the bytecode VM into a genuine +second compilation target (which moved a great deal this session: it went from +crashing on most programs to running the core language *with consent enforced +and closures that capture state*) and reconciling the stale documentation and +scope numbers. Everything past that is the WISH horizon. + +The one honest asterisk: `STATE.a2ml` pegs whole-vision completion at *~35%* — +that figure counts the entire surface language plus full tooling plus ecosystem +(the large WISH/INTEND surface), so it coexists with "the core MUSTs hold." The +gap between "MUSTs met" and "35%" *is* the roadmap above. + +== Provenance + +Work merged to `main` that this affirmation reflects: + +* PR #90 — Lean array typing (mirror of Coq `T_Array` / `T_Lit_Array`) +* PR #91 — statement typing judgment + metatheory (Lean + Coq) +* PR #92 — VM: full expression coverage + Result/record/index execution + consent enforcement under `#care` +* PR #93 — VM: Result constructors from surface syntax + closures +* PR #94 — VM: upvalue capture for closures + +Deeper detail: `docs/proofs/verification/AUDIT.md` (proofs) and the per-PR +descriptions. Next-session handoff: `docs/NEXT-CLAUDE-PROMPT.md`. + +// Affirmed 2026-06-19 (UTC date) in an AI-assisted Claude Code session, on +// behalf of the maintainer. Reconcile against hyperpolymath/standards. diff --git a/docs/NEXT-CLAUDE-PROMPT.md b/docs/NEXT-CLAUDE-PROMPT.md new file mode 100644 index 0000000..cf73588 --- /dev/null +++ b/docs/NEXT-CLAUDE-PROMPT.md @@ -0,0 +1,72 @@ + +# WokeLang — handoff prompt for the next Claude + +Paste the block below into a fresh Claude Code session working on +`hyperpolymath/wokelang`. (State as of 2026-06-19 — see `AFFIRMATION.adoc`.) + +--- + +You are continuing work on **WokeLang**, a consent-driven, human-centred +programming language. Primary implementation is **Rust** (`src/`), with an +**OCaml** reference core (`core/`) and formal proofs in **Lean/Coq** +(`docs/proofs/verification/`) and **Idris 2** (`src/abi/`). Match the +interpreter (`src/interpreter/mod.rs`) as the reference semantics. + +**Read first, in order:** +1. `AFFIRMATION.adoc` — the current MUST / INTEND / WISH standing (timestamped). +2. `.machine_readable/6a2/STATE.a2ml` — project state checkpoint. +3. `docs/proofs/verification/AUDIT.md` — proof state (Lean / Coq / Idris). +4. `PROOF-NEEDS.md`, `TEST-NEEDS.md`, `TOOLCHAIN-WISHLIST.md` — needs and wishes. + (Note: `TOOLCHAIN-WISHLIST.md` is **stale** — LSP, the DAP debugger, and the + WASM backend already exist; and it says 85% complete while `STATE.a2ml` says + 35%. Reconciling these is itself an open task.) + +**Where things stand (2026-06-19):** +- **Proofs.** Lean + Coq at parity (expression-core type safety + arrays + + statement typing) and an Idris consent calculus (typing with a handler + context + small-step with an audit log + `progress`). CI-gated + (`lean-proofs.yml`, `coq-proofs.yml`), `sorry`/axiom-free. +- **Bytecode VM** (`src/vm/`). Now runs the core language: Result types, + records, indexing, control flow, **consent enforcement under `#care`** + (deny-by-default), and **closures with upvalue capture**. 188 lib tests green. + It went from crashing on most programs to running the core language this + session (PRs #92–#94). + +**Best next steps (near-horizon, mostly independent — pick one):** +- *VM → real compilation target:* + - **Interpreter↔VM parity harness:** run each `conformance/*.woke` and + `examples/*.woke` through both the interpreter and `vm::run_vm`, assert + equal results, CI-gate it. (Highest-value correctness mechanism.) + - **`.wbc` bytecode serialization:** `woke compile -o x.wbc` cannot write a + loadable file yet (`src/main.rs` says "not yet implemented"); add serde + round-trip so `woke run-vm x.wbc` loads it. + - **Consent grant-sources:** seed the VM's `granted` set (in `src/vm/machine.rs`) + from `superpower` declarations so `#care` programs can actually grant + capabilities (currently deny-by-default). + - **Worker statements on the VM** (the 5 concurrency forms — needs a VM + channel/scheduler model). + - **By-reference + multi-level closure capture** (current capture is by-value, + single-level). +- *Proofs:* **float arithmetic** variants; **open-term expression preservation** + (the prerequisite for statement *dynamic* safety); decide the **eval ↔ spec + correspondence** question (PROOF-NEEDS #2) with the maintainer. +- *Docs:* **reconcile** `README.adoc` / `EXPLAINME.adoc` / `TOOLCHAIN-WISHLIST.md` + to reality and fix the 35%-vs-85% completion contradiction. + +**Conventions & CI gates:** +- Develop on the branch you are told to; push and open a **draft PR**. +- Gates include **Build Check** (`cargo fmt --check` + `cargo clippy --lib --bins + -- -D warnings`), **Build + E2E (Rust + OCaml)**, **lean-proofs**, **coq-proofs**. + **Run `cargo fmt` + `cargo clippy --lib --bins -- -D warnings` locally before + pushing** — Build Check gates on both, and that has bitten past sessions. +- Language policy (`.claude/CLAUDE.md`): Rust / OCaml / Lean / Coq / Idris as + present; no Go / Python / TypeScript; `Containerfile`, not `Dockerfile`. +- Keep proofs `sorry`/axiom-free; pin each headline theorem the way `AUDIT.md` + describes. + +Tell me which item to take, or propose one and go. + +---