Skip to content

Commit 4cd7bb1

Browse files
claudeclaude
committed
docs(readme): update README.md from stale stub to full landing page
README.md was a stale "code has been moved" stub from an earlier repo migration. GitHub displays README.md over README.adoc, so the canonical landing page was broken. Rewrite README.md with accurate content matching README.adoc: proof status table, echo type integration, quickstart for Coq/Idris2, companion repos table. Also remove the "This README replaces an earlier stub" note from README.adoc (no longer relevant now both files are current) and retitle it as the AsciiDoc edition. https://claude.ai/code/session_01VHjceAPA5ZARUe7ESWNQPF
1 parent c3b8d79 commit 4cd7bb1

2 files changed

Lines changed: 119 additions & 6 deletions

File tree

‎README.adoc‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
// SPDX-License-Identifier: MPL-2.0
22
// Copyright (c) 2026 Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
33

4-
= my-lang
4+
= my-lang (AsciiDoc edition)
55
:author: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
66
:revdate: 2026-06-02
77
:toc: left

‎README.md‎

Lines changed: 118 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,121 @@
1-
# My-Lang
1+
<!-- SPDX-License-Identifier: MPL-2.0 -->
2+
<!-- Copyright (c) 2026 Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> -->
23

3-
This code has been moved to the canonical repository:
4-
https://github.com/hyperpolymath/my-lang
4+
# my-lang
55

6-
Canonical location: ~/Documents/hyperpolymath-repos/my-lang/
6+
`my-lang` is the *next-generation language* working project — a multi-dialect
7+
surface for the hyperpolymath language stack. It is one of two flagship language
8+
experiments in the estate (the other being
9+
[`affinescript`](https://github.com/hyperpolymath/affinescript)). The two
10+
projects are *siblings*, not a fork — they share design principles but diverge
11+
in dialect scope and proof strategy.
712

8-
This directory is kept as a reference stub only.
13+
For a gentler entry point see [EXPLAINME.adoc](EXPLAINME.adoc).
14+
15+
## What's in here
16+
17+
| Path | Contents |
18+
|------|----------|
19+
| `crates/` | Rust compiler crates. `crates/my-lang/src/types.rs` is the type checker, including `EchoMode`, `Ty::Echo`, and full affine-weakening semantics. |
20+
| `dialects/` | Per-dialect surface-syntax definitions: *solo* (affine, single-agent), *duet* (session-typed), *ensemble* (multi-agent), *me* (visual/pedagogic). |
21+
| `proofs/` | Formal verification assets — paper proofs, mechanised Coq + Idris2 solo-core. See [`proofs/STATUS.md`](proofs/STATUS.md) for the authoritative proof-status registry. |
22+
| `conformance/` | Conformance tests — programs any compliant implementation must accept or reject identically. |
23+
| `examples/` | Worked examples for each dialect. |
24+
| `docs/` | Design notes, ADRs. Includes the [echo-types integration design note](docs/design/echo-types-integration.md). |
25+
| `frontier-practices/` | Forward-looking research experiments (not shipped). |
26+
| `contractiles/` | Project-level Mustfile / Dustfile invariant and recovery contracts. |
27+
28+
## Quickstart
29+
30+
```bash
31+
git clone git@github.com:hyperpolymath/my-lang.git
32+
cd my-lang
33+
34+
just build # builds the workspace (Rust)
35+
just test # runs unit + conformance tests
36+
```
37+
38+
To check the Coq solo-core:
39+
40+
```bash
41+
cd proofs/verification/coq/solo-core
42+
coq_makefile -f _CoqProject -o CoqMakefile && make -f CoqMakefile
43+
```
44+
45+
To check the Idris2 solo-core:
46+
47+
```bash
48+
cd proofs/verification/idris/solo-core
49+
idris2 --check solo-core.ipkg
50+
```
51+
52+
## Proof and verification status
53+
54+
`my-lang` follows a *statements-first, machine-checked later* proof methodology
55+
mirroring `affinescript`'s solo-core approach.
56+
[`proofs/STATUS.md`](proofs/STATUS.md) is the single authoritative source — no
57+
proof is described as "proved" there until a proof assistant accepts it.
58+
59+
**Current state (2026-06-02):**
60+
61+
| Artefact | Status |
62+
|----------|--------|
63+
| QTT semiring + laws (Coq + Idris2) | *locally-checked* — all laws proved by exhaustive case analysis |
64+
| Solo syntax, contexts, typing (Coq + Idris2) | *definitions-only* |
65+
| Progress / Preservation | *statement-only* — Phase F1.3/F1.4 |
66+
| Echo type former (`EchoMode`, `Ty::Echo`, weakening) | *locally-checked* — 5 Agda-mirroring unit tests |
67+
| Paper proofs (~6.3k lines) | *proved-on-paper* |
68+
| Proof CI | *absent* — Phase F5 |
69+
70+
See [`proofs/ALIGNMENT-PLAN.md`](proofs/ALIGNMENT-PLAN.md) for the phased
71+
roadmap toward AffineScript parity.
72+
73+
## Echo type integration
74+
75+
`my-lang` integrates the [`echo-types`](https://github.com/hyperpolymath/echo-types)
76+
Agda library — a formal account of *loss that is not total erasure*.
77+
78+
```
79+
Echo<A => B> // "a proof-relevant residue of a lossy collapse from A to B"
80+
```
81+
82+
`EchoMode { Linear, Affine }` mirrors the `EchoLinear.agda` two-point poset
83+
`linear ⊑ affine`. A `Linear` echo may be weakened to `Affine` (one-way, no
84+
section). Domain and codomain are invariant under subtyping.
85+
86+
**Claim boundary** (retraction R-2026-05-18):
87+
> Echo is a *loss-graded reindexing modality over a thin poset*, not a graded
88+
> comonad or free construction.
89+
90+
Full design rationale: [`docs/design/echo-types-integration.md`](docs/design/echo-types-integration.md).
91+
92+
## Architectural authority
93+
94+
- [`ANCHOR.scope-arrest.*`](ANCHOR.scope-arrest.2026-01-01.Jewell.scm) — the scope-arrest anchor enumerating what `my-lang` will and will not be.
95+
- [`AUTHORITY_STACK.mustfile-nickel.scm`](AUTHORITY_STACK.mustfile-nickel.scm) — the cross-cutting authority stack.
96+
97+
Consult these before opening a feature request.
98+
99+
## Status
100+
101+
- **Licence**: MPL-2.0
102+
- **Maturity**: design-iteration / early alpha. Working Rust compiler core exists (137+ passing tests); surface syntax and semantics still settling.
103+
- **Proof phase**: F1.0 complete — QTT semiring proved on dual Coq + Idris2 tracks; soundness statements committed.
104+
- **Governance**: CI green on all shipped checks; proof CI (Phase F5) pending.
105+
106+
## Contributing
107+
108+
See [CONTRIBUTING.adoc](CONTRIBUTING.adoc). GPG-signed commits required.
109+
Language policy, package management, and security requirements are enforced by
110+
the estate governance workflow (`hyperpolymath/standards`). New contributors
111+
should read [EXPLAINME.adoc](EXPLAINME.adoc) first.
112+
113+
## Companion repositories
114+
115+
| Repository | Relationship |
116+
|------------|-------------|
117+
| [`hyperpolymath/standards`](https://github.com/hyperpolymath/standards) | Estate-wide standards and governance |
118+
| [`hyperpolymath/affinescript`](https://github.com/hyperpolymath/affinescript) | Sibling language; target parity state defined in `proofs/ALIGNMENT-PLAN.md` |
119+
| [`hyperpolymath/echo-types`](https://github.com/hyperpolymath/echo-types) | Upstream Agda echo-types library integrated into the type checker |
120+
| [`hyperpolymath/EchoTypes.jl`](https://github.com/hyperpolymath/EchoTypes.jl) | Julia companion; planned differential oracle for echo type testing |
121+
| [`hyperpolymath/typed-wasm`](https://github.com/hyperpolymath/typed-wasm) | Shared typed-wasm compilation backend |

0 commit comments

Comments
 (0)