|
| 1 | +// SPDX-License-Identifier: MPL-2.0 |
| 2 | +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | += Aspect-Oriented Language Design (AOLD) |
| 4 | +Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 5 | +:toc: left |
| 6 | +:toclevels: 3 |
| 7 | +:icons: font |
| 8 | + |
| 9 | +[.lead] |
| 10 | +**AOLD is the design philosophy behind the -iser family.** Instead of choosing |
| 11 | +one general-purpose language and living with its global trade-offs, AOLD treats |
| 12 | +each specialist language's _unique strength_ as a weavable **aspect** that you |
| 13 | +can bolt onto an existing codebase on demand — and remove just as easily. |
| 14 | + |
| 15 | +== The problem AOLD answers |
| 16 | + |
| 17 | +Every language makes one global bet. Chapel bets everything on distributed |
| 18 | +data-parallelism; Pony on data-race-free actors; Dafny on |
| 19 | +correct-by-construction proof; Futhark on GPU array kernels; OTP on |
| 20 | +fault-tolerant supervision. Each is _extraordinary_ at its one thing and |
| 21 | +ordinary (or absent) at everything else. |
| 22 | + |
| 23 | +In practice that bet is hard to take: |
| 24 | + |
| 25 | +. **Steep learning curve** — to get the superpower you must rewrite in, or deeply |
| 26 | + learn, the specialist language. |
| 27 | +. **All-or-nothing adoption** — there is rarely an incremental path; you commit |
| 28 | + the whole system or none of it. |
| 29 | +. **Integration tax** — wiring the specialist runtime into your existing |
| 30 | + Rust/C/Zig project is non-trivial and easy to get subtly wrong. |
| 31 | + |
| 32 | +So the superpowers stay locked behind their languages, and most projects never |
| 33 | +touch them. |
| 34 | + |
| 35 | +== The core idea: languages as aspects |
| 36 | + |
| 37 | +AOLD unlocks the superpower _without_ taking the global bet. An **-iser** is a |
| 38 | +Rust CLI that injects exactly one specialist language's capability into the code |
| 39 | +you already write, through a uniform, proof-carrying pipeline: |
| 40 | + |
| 41 | +[literal] |
| 42 | +.... |
| 43 | + your manifest ──► Idris2 ABI ──► Zig FFI ──► target-language codegen ──► build / run |
| 44 | + (what you want) (prove the (C-ABI (emit the specialist (you never |
| 45 | + interface) bridge) language's code) wrote any) |
| 46 | +.... |
| 47 | + |
| 48 | +You describe _what_ you want in a declarative TOML manifest. The -iser validates |
| 49 | +it against a formally verified **Idris2 ABI**, bridges to your application across |
| 50 | +a **Zig FFI** seam, generates the specialist-language code, and builds it. You |
| 51 | +get the aspect; you never learn the language. |
| 52 | + |
| 53 | +== The "mech suit" mental model |
| 54 | + |
| 55 | +The cleanest way to think about an -iser is as a **mech suit for your |
| 56 | +application**. Your program/database/tool stays exactly what it is — its own |
| 57 | +language, its own logic. The -iser is an _exoskeleton_ that grants it one exotic |
| 58 | +capability it did not have: distribution, GPU acceleration, data-race freedom, |
| 59 | +fault tolerance, machine-checked correctness, energy-awareness, reversibility. |
| 60 | + |
| 61 | +Three properties make it a suit rather than a rewrite: |
| 62 | + |
| 63 | +* **Addable** — you bolt it on around the existing code, at the boundary. |
| 64 | +* **Removable / reversible** — take the suit off and the original program is |
| 65 | + unchanged. Nothing is load-bearing on the aspect that cannot be unwound. |
| 66 | +* **Composable** — suits stack. See `iSOS.adoc` for how multiple aspects layer |
| 67 | + on one host (the _Integrated Stack of Stacks_). |
| 68 | + |
| 69 | +== What AOLD is _not_ |
| 70 | + |
| 71 | +[cols="1,3",options="header"] |
| 72 | +|=== |
| 73 | +| It is not… | …because |
| 74 | + |
| 75 | +| aggregate-library (aLib) |
| 76 | +| aLib is the **dual** of AOLD. aLib finds the minimal _overlap_ common to all |
| 77 | + systems (subtractive: the greatest common denominator, conformance-tested). |
| 78 | + AOLD adds the exotic _differentiator_ of one system (additive: the specialist |
| 79 | + edge). aLib reduces to the shared core; -isers extend with the rare capability. |
| 80 | + |
| 81 | +| the dyadic toolchain/language design of Ephapax |
| 82 | +| Ephapax is about the design of a single language and its paired toolchain. |
| 83 | + AOLD is about _weaving many languages' aspects_ onto a foreign host. |
| 84 | + |
| 85 | +| an AffineScript-style "face" |
| 86 | +| A "face" is a uniform surface over a substrate. An aspect is a _capability |
| 87 | + injection_ at a proof-carrying seam, not a presentation layer. |
| 88 | + |
| 89 | +| nextgen-language-evangeliser |
| 90 | +| That project advocates for next-generation languages as wholes. The -iser |
| 91 | + atlas (`ATLAS.adoc`) routes you to a _capability_, not to a language to adopt. |
| 92 | +|=== |
| 93 | + |
| 94 | +== The aspect taxonomy |
| 95 | + |
| 96 | +Each -iser is one aspect. The family is the palette. |
| 97 | + |
| 98 | +[cols="2,3,2",options="header"] |
| 99 | +|=== |
| 100 | +| -iser | Aspect (the superpower it weaves in) | Host gains |
| 101 | + |
| 102 | +| typedqliser | Formal type safety (10 graded levels) over a query language | injection-/null-/schema-safe queries |
| 103 | +| chapeliser | Chapel distributed data-parallelism | single-machine workload → cluster |
| 104 | +| verisimiser | VeriSimDB octad capabilities | drift / provenance / temporal over any DB |
| 105 | +| julianiser | Julia numerical performance | 100× speedups for Python/R pipelines |
| 106 | +| futharkiser | Futhark GPU array kernels | data-parallel ops → GPU |
| 107 | +| idrisiser | Idris2 dependent-type proofs | proven-correct wrappers from interfaces |
| 108 | +| dafniser | Dafny correct-by-construction | verified critical functions |
| 109 | +| tlaiser | TLA+/PlusCal model checking | state machines checked for safety/liveness |
| 110 | +| alloyiser | Alloy relational model finding | formal models from API specs |
| 111 | +| lustreiser | Lustre synchronous dataflow | verified real-time embedded code |
| 112 | +| ponyiser | Pony reference capabilities | data-race freedom for concurrent code |
| 113 | +| otpiser | OTP/BEAM supervision | fault-tolerance trees, let-it-crash resilience |
| 114 | +| halideiser | Halide schedule optimisation | optimised image/video pipelines |
| 115 | +| bqniser | BQN array primitives | array patterns rewritten as optimised idioms |
| 116 | +| nimiser | Nim metaprogramming | high-performance C libraries |
| 117 | +| atsiser | ATS linear types | zero-cost memory safety wrapping C |
| 118 | +| affinescriptiser | AffineScript affine + dependent types | WASM-targeted resource safety |
| 119 | +| a2mliser | A2ML cryptographic attestation | tamper-evident markup / configuration |
| 120 | +| ephapaxiser | Ephapax single-use linear semantics | enforce use-exactly-once on resources |
| 121 | +| eclexiaiser | Eclexia cost modelling | energy / carbon / resource-cost awareness |
| 122 | +| k9iser | K9 contracts | configs become self-validating |
| 123 | +| oblibeniser | Oblíbený reversibility | operations made reversible + auditable |
| 124 | +| phronesiser | Phronesis ethical constraints | provably-safe guardrails for AI agents |
| 125 | +| wokelangiser | WokeLang consent + a11y patterns | consent flows and accessibility |
| 126 | +| betlangiser | Betlang ternary probabilistic modelling | uncertainty over deterministic code |
| 127 | +| mylangiser | My-Lang progressive disclosure | layered interfaces over complex APIs |
| 128 | +| anvomidaviser | Anvomidav ISU notation | figure-skating programs as formal artefacts |
| 129 | +|=== |
| 130 | + |
| 131 | +`iseriser` is the meta-framework that scaffolds new aspects into this palette. |
| 132 | + |
| 133 | +== The proof-carrying seam |
| 134 | + |
| 135 | +An aspect is only worth bolting on if its guarantee survives the journey into |
| 136 | +your host. AOLD makes that survivable by construction: |
| 137 | + |
| 138 | +* The **Idris2 ABI** is where the aspect's invariant is _proven_ — e.g. |
| 139 | + chapeliser proves `PartitionComplete` (every item is placed) and |
| 140 | + `PartitionDisjoint` (no item is placed twice) and `GatherConservation` |
| 141 | + (no result is lost). |
| 142 | +* The **Zig FFI** is the zero-overhead C-ABI bridge that carries data across the |
| 143 | + boundary without re-introducing unsafety. |
| 144 | +* **invariant-path** is the conscience: it _traces the proven invariant across |
| 145 | + the seam into the host_ and flags any point where the guarantee is silently |
| 146 | + over-generalised (the classic `theorem → guarantee → "universal claim"` |
| 147 | + slide). See `iSOS.adoc`. |
| 148 | + |
| 149 | +== See also |
| 150 | + |
| 151 | +* `iSOS.adoc` — how aspects compose into an Integrated Stack of Stacks. |
| 152 | +* `../ATLAS.adoc` — the routing map: pick the -iser for your need. |
| 153 | +* `../../README.adoc` — the family overview and install/usage. |
0 commit comments