|
3 | 3 |
|
4 | 4 | = RSR Language Policy |
5 | 5 | :author: Jonathan D.A. Jewell (hyperpolymath) |
6 | | -:revnumber: 1.1.0 |
7 | | -:revdate: 2026-04-10 |
| 6 | +:revnumber: 1.2.0 |
| 7 | +:revdate: 2026-05-16 |
8 | 8 | :toc: left |
9 | 9 | :icons: font |
10 | 10 | :source-repo: https://github.com/hyperpolymath/cccp |
11 | 11 |
|
12 | 12 | [NOTE] |
13 | 13 | ==== |
14 | | -*Version Status*: v1.1.0 — allowed/banned lists amended 2026-04-10. See §Amendments |
15 | | -at the bottom of this document for the rationale and the full change list. The |
16 | | -prior v1.0.0 freeze was lifted on the same date. |
| 14 | +*Version Status*: v1.2.0 — codifies the Interface & Architecture Law |
| 15 | +(ABI=Idris2, API+FFI=Zig; strict typed boundaries; no gatekeeperless gateways) |
| 16 | +as a normative section, 2026-05-16. v1.1.0 amended the allowed/banned lists |
| 17 | +2026-04-10. See §Amendments at the bottom for rationale and the full change list. |
17 | 18 | ==== |
18 | 19 |
|
19 | 20 | == Terminology: "Rust" means "Rust/SPARK" |
@@ -239,6 +240,54 @@ the reach order is: |
239 | 240 | consideration) |
240 | 241 | * `Node.js` as a standalone runtime — replaced by Deno |
241 | 242 |
|
| 243 | +== Interface & Architecture Law (NORMATIVE) |
| 244 | + |
| 245 | +This is a day-1, estate-wide structural law. It is non-negotiable and applies |
| 246 | +to *every* repository. |
| 247 | + |
| 248 | +=== Layer languages |
| 249 | + |
| 250 | +* **ABI layer → Idris2** (`src/abi/*.idr`): formal types + proofs. Always. |
| 251 | +* **FFI layer → pure Zig** (`ffi/zig/`). Always — since day 1. |
| 252 | +* **API layer → pure Zig** (`src/api/zig/`). Always — since V was dropped for APIs. |
| 253 | + |
| 254 | +Rust/SPARK is *application* logic only (per §Terminology); it is **never** the |
| 255 | +ABI, API, or FFI layer, and is **never** the target of an abi/api/ffi migration. |
| 256 | +C is never an estate API/ABI/FFI layer either. A `MIGRATION.adoc`, `CLAUDE.md`, |
| 257 | +manifest comment, or build file that says "→ Rust" / "canonical Rust rewrite of |
| 258 | +the API" is **itself off-policy drift**: the canonical target is the Zig |
| 259 | +implementation. Stray `src/api/rust/` API crates are debt to remove, not a |
| 260 | +destination. Consumers may still *call* the C ABI from any language — that is |
| 261 | +consumer-side binding, not the layer implementation. |
| 262 | + |
| 263 | +=== V-lang only when it is Coq |
| 264 | + |
| 265 | +V-lang is banned (see §Banned Languages); the migration target is **Zig, never |
| 266 | +Rust**. The sanctioned exception is the `developer-ecosystem/v-ecosystem/` |
| 267 | +subtree (and `awesome-v`, a curated list — never touched). Outside those, a `.v` |
| 268 | +file or "V" reference in code, docs, `CLAUDE.md`, `Justfile`, `Containerfile`, |
| 269 | +or `flake.nix` is acceptable **only when it is a Coq/Rocq proof** |
| 270 | +(`Require Import` / `Theorem` / `Qed.`). All other V references are drift to |
| 271 | +remove. V-stub-generation recipes are *re-emergence engines* and must be |
| 272 | +deleted, not merely disabled. |
| 273 | + |
| 274 | +=== Strict typed boundaries |
| 275 | + |
| 276 | +Every cross-language or cross-trust boundary MUST be type-protected and |
| 277 | +correctness-gated: an **Idris2 correctness contract** (proven ABI/protocol) plus |
| 278 | +a **Zig transaction interface** (the marshalling / C-ABI / wire layer). This |
| 279 | +covers in-process FFI, NIFs (exemplar: the `snifs` repo), WASM boundaries |
| 280 | +(exemplar: the `typed-wasm` repo), API gateways, gRPC/GraphQL/REST edges, DB and |
| 281 | +service connectors, and any (de)serialisation trust boundary. An |
| 282 | +untyped/unproven boundary is non-conformant and blocks. |
| 283 | + |
| 284 | +=== No gatekeeperless gateways |
| 285 | + |
| 286 | +Every gateway / API edge MUST front a policy gate (authentication + entitlement |
| 287 | ++ rate-limiting). A gateway without a gatekeeper is a defect, not a later-phase |
| 288 | +nicety. (This is a *runtime access-control* rule and is distinct from the |
| 289 | +social "graduated trust without gatekeeping" contribution model.) |
| 290 | + |
242 | 291 | == Machine-Readable Policy |
243 | 292 |
|
244 | 293 | See link:../spec.scm/language-policy.scm[spec.scm/language-policy.scm] for tooling integration. |
|
0 commit comments