|
1 | 1 | # SPDX-License-Identifier: PMPL-1.0-or-later |
2 | 2 | # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
3 | 3 | # |
4 | | -# STATE.a2ml — Project state checkpoint |
5 | | -# The Agent Meta-Language: 007-lang |
6 | | - |
7 | | -[metadata] |
8 | | -project = "007-lang" |
9 | | -version = "0.1.0" |
10 | | -last-updated = "2026-03-30" |
11 | | -status = "active" # active | paused | archived |
12 | | - |
13 | | -[project-context] |
14 | | -name = "007-lang" |
15 | | -purpose = "The Agent Meta-Language — a language for agents that make agents. Six pillars: Harvard architecture, actors, capabilities, session types, linear handles, choreographies." |
16 | | -completion-percentage = 55 |
17 | | - |
18 | | -[position] |
19 | | -phase = "audit-remediation" # design | implementation | testing | maintenance | archived |
20 | | -maturity = "alpha" # experimental | alpha | beta | production | lts |
21 | | - |
22 | | -[route-to-mvp] |
23 | | -milestones = [ |
24 | | - { name = "Phase 0: EBNF specification draft", completion = 90 }, |
25 | | - { name = "Phase 1: Pest parser (core grammar)", completion = 60 }, |
26 | | - { name = "Phase 2: Tree-walking evaluator (layers 1-4)", completion = 70 }, |
27 | | - { name = "Phase 3: Parser gap fill (types, imports, reversibility, locales, choreographies)", completion = 10 }, |
28 | | - { name = "Phase 4: Full evaluator (layers 5-8)", completion = 0 }, |
29 | | - { name = "Phase 5: BEAM codegen prototype", completion = 0 }, |
30 | | - { name = "Phase 6: WASM/native secondary targets", completion = 0 }, |
31 | | - { name = "Phase 7: Formal proofs of session type soundness", completion = 0 }, |
32 | | -] |
33 | | - |
34 | | -[blockers-and-issues] |
35 | | -issues = [ |
36 | | - "Public docs and papers still overstate maturity in places", |
37 | | - "Clippy does not pass cleanly across the workspace", |
38 | | - "Known proof debt remains around Harvard and broader soundness claims", |
39 | | -] |
40 | | - |
41 | | -[critical-next-actions] |
42 | | -actions = [ |
43 | | - "Tighten public claims and manuscript front matter to match current evidence", |
44 | | - "Fix clippy failures and warning hotspots in live Rust crates", |
45 | | - "Add an explicit aspect-test surface to the task runner", |
46 | | - "Continue parser gaps, soundness work, and Harvard/session proof closure", |
47 | | -] |
48 | | - |
49 | | -[maintenance-status] |
50 | | -last-run-utc = "never" |
51 | | -last-report = "docs/reports/maintenance/latest.json" |
52 | | -last-result = "fail" # unknown | pass | warn | fail |
53 | | -open-warnings = 2 |
54 | | -open-failures = 1 |
55 | | - |
56 | | -[crg] |
57 | | -grade = "C" |
58 | | -achieved = "2026-04-04" |
59 | | -evidence = [ |
60 | | - "unit: 728 passing tests in oo7-core + sub-crates", |
61 | | - "smoke: parser_tests + eval_tests (point tests)", |
62 | | - "p2p: crates/oo7-core/tests/property_tests.rs (5 proptest properties)", |
63 | | - "e2e: crates/oo7-core/tests/e2e_tests.rs (6 full-pipeline tests)", |
64 | | - "aspect: crates/oo7-core/tests/aspect_tests.rs (6 cross-cutting tests)", |
65 | | - "contract: contracts.rs module + typechecker check_program", |
66 | | - "benchmarks: criterion toolchain_bench + algebraic_dispatch_bench", |
67 | | -] |
68 | | - |
69 | | -[ecosystem] |
70 | | -part-of = ["nextgen-languages ecosystem"] |
71 | | -depends-on = ["pest", "clap"] |
| 4 | +# STATE.a2ml v2 — Thin Session Journal for 007-lang |
| 5 | +# See: standards/a2ml-templates/STATE.a2ml.v2.spec.adoc |
| 6 | + |
| 7 | +@state(version="2.0"): |
| 8 | +phase: "implementation" |
| 9 | +next_action: "Complete parser gap fill (types, imports, reversibility, locales, choreographies)" |
| 10 | +last_action: "PataCL/JtV overlap audit completed 2026-04-27 — 007 is NOT a current PataCL host (see [patacl-relationship])" |
| 11 | +updated: 2026-04-27T00:00:00Z |
| 12 | + |
| 13 | +@blockers: |
| 14 | +- id: clippy-drift |
| 15 | + description: "Clippy does not pass cleanly across the workspace" |
| 16 | + since: 2026-03-30 |
| 17 | +- id: proof-debt |
| 18 | + description: "Harvard and broader soundness claims require formal Idris2 proof closure" |
| 19 | + since: 2026-03-30 |
| 20 | +@end |
| 21 | + |
| 22 | +@note(id="patacl-relationship", added="2026-04-27"): |
| 23 | +PataCL (PataCompiler Language) was audited for 007 applicability. Key decisions: |
| 24 | + |
| 25 | +SHARED FOUNDATION (no transfer needed): |
| 26 | +- Harvard binary split (Control/Data) — present independently in both |
| 27 | +- @total/@pure purity discipline — both enforce it (007 adds @neural tier) |
| 28 | +- Idris2 + Rocq proof infrastructure — both have it independently |
| 29 | + |
| 30 | +`given` CLAUSE — KEEP SOFT (deliberate): |
| 31 | + 007 `given` is structurally close to a PataCL predicate (data-exprs, Total purity) |
| 32 | + but is EXPLICITLY a "suggestion not a guard" (de Man parabasis — interpretive |
| 33 | + freedom). DO NOT harden `given` into a PataCL fact-environment gate. The softness |
| 34 | + is a design commitment, not an oversight. |
| 35 | + |
| 36 | +`@sentinel` — COMPLEMENTARY (not competing): |
| 37 | + Hard compile-time integrity gate (hashes grammar/type rules). Post-hoc integrity |
| 38 | + check rather than pre-condition fact-env gate. Both can coexist if 007 ever needs |
| 39 | + cross-target dispatch. |
| 40 | + |
| 41 | +FUTURE ADOPTION — CONDITIONAL: |
| 42 | + 007 could become a Phase 6 PataCL host IF it adds compile-time backend-selection |
| 43 | + constructs for Tier 5 coprocessors (CUDA/Vulkan/Metal/FPGA). Currently these are |
| 44 | + runtime interpreter backends, not language-level declarations — no trigger yet. |
| 45 | + Organic need is the right trigger; do not force it. |
| 46 | +@end |
| 47 | +@end |
0 commit comments