Origin
docs/ROADMAP.md Stage 6 ("Cross-prover semantics — translation actually works"), row 6a:
Stage 6 Cross-prover semantics translation actually works
6a OpenTheory bridge real bidirectional term translation
Stage 6 is Q3-Q4 2026 territory per the 8-stage map (Stage 5 is the current "next sprint" after S1-S5; Stage 6 follows). Per the long-tail enumeration this is ~15 PRs of work.
Scope
Replace the current stub at src/rust/exchange/ (OpenTheory listed under v1.5 "cross-prover proof exchange" but not yet performing real bidirectional term translation) with a real OpenTheory article emitter + ingester:
- Article serialiser for terms produced by ECHIDNA's
core::Term
- Article parser into
core::Term
- Round-trip property tests against the OpenTheory standard library
- Conformance against the OpenTheory CI suite
Estimated ~15 PRs (per long-tail roadmap enumeration).
Dependencies
- Stage 5 must land first (Cap'n Proto IPC + Chapel + Tier-4 CI) for the dispatcher to actually call the bridge in anger
- No upstream blocker — OpenTheory tooling is in Debian/Guix
Why filed
To make the ROADMAP.md Stage 6a commitment trackable as a distinct work item; today it lives only as a single ASCII-art row with no issue, no milestone, no owner. Stage 6 is the lingua-franca play for the platform and deserves a visible long-tail tracker so the owner can size the v2.x release.
Origin
docs/ROADMAP.mdStage 6 ("Cross-prover semantics — translation actually works"), row 6a:Stage 6 is Q3-Q4 2026 territory per the 8-stage map (Stage 5 is the current "next sprint" after S1-S5; Stage 6 follows). Per the long-tail enumeration this is ~15 PRs of work.
Scope
Replace the current stub at
src/rust/exchange/(OpenTheory listed under v1.5 "cross-prover proof exchange" but not yet performing real bidirectional term translation) with a real OpenTheory article emitter + ingester:core::Termcore::TermEstimated ~15 PRs (per long-tail roadmap enumeration).
Dependencies
Why filed
To make the ROADMAP.md Stage 6a commitment trackable as a distinct work item; today it lives only as a single ASCII-art row with no issue, no milestone, no owner. Stage 6 is the lingua-franca play for the platform and deserves a visible long-tail tracker so the owner can size the v2.x release.