Ephapax

ἐφάπαξ — once for all.

Important

Not to be confused with AffineScript

This is Ephapax, a research language for WebAssembly memory safety. It is not AffineScript, a separate language at hyperpolymath/affinescript that succeeds JS / TS / AffineScript.

The two share exactly one thing: both target typed-wasm. They have separate ASTs, separate type checkers, separate compilers, separate proof stories. The word affine overlaps in both names because it names a substructural- logic property — that’s a logic-family fact, not a project relationship.

Internal note: Ephapax is itself dyadic — ephapax-linear (strict core) and ephapax-affine (versatile prototyping companion) are both inside this repo, one Rust crate, one AST, two structural disciplines. ephapax-affine is not AffineScript. When ambiguous, write "ephapax-affine sublanguage" vs "AffineScript language".

Canonical disambiguation (read this before applying any cross-repo lesson): nextgen-languages/docs/disambiguation/ephapax-vs-affinescript.md.

Note

🌱 Ephapax is gestating — second-draft in progress; proof redesign required (start with V1-TO-V2.adoc)

This language is in a deliberate second-draft process. Grammar work is active; the proof track has preserved a false legacy theorem and discovered further L1/L2 gaps that require redesign. The full status is in V1-TO-V2.adoc and PROOF-NEEDS.adoc.

The grammar (v1 → v2). The flat v1 surface worked for the core but could not grow into modules / generics / effects / comptime. v2 adds the missing layer — surface → desugar → core — and is landing in phases, tests green (spec/ephapax-v2-grammar.ebnf + the v2_grammar_phase_* suite).

The soundness proof (v1 → v2). On 2026-05-26 a machine-checked Coq counterexample (formal/Counterexample.v, then 5 Qed lemmas, now 6 with preservation_false) proved that preservation as stated in the legacy single-judgment design is unsound — a region exit could invalidate a sibling’s assumptions untracked. Discovering that with a proof, before anyone depended on it, is the rare correct thing, not a failure. The four-layer architecture is a design program, not an established preservation result. The legacy statement is retired to preservation_stmt : Prop and refuted by Counterexample.preservation_false; the no-False gate rejects any Admitted, so it must not be restored. Later pinned counterexamples also refute the unrestricted L1 preservation claim. There is no unconditional L2 preservation theorem, while the L2 β-case helpers are conditional. L3’s preservation_l3 and case lemmas are Qed for matching echo-emitting rule pairs only; L4 is a Phase A scaffold.

For anyone (human or bot) doing the work: preserve every pinned counterexample and do not attempt to prove a refuted statement. Active proof work means specifying and proving sound replacements locally for Ephapax’s own syntax, judgments, and steps—not relying on shared vocabulary or an upstream repository. Authoritative maps: V1-TO-V2.adoc (the frame), STATUS.adoc (operational past/present/future), formal/PRESERVATION-DESIGN.adoc (four-layer architecture), PROOF-NEEDS.adoc (proof debt + do-not-do list). Anything dated before 2026-05-26 describing a "preservation closure plan" or "910 → 12 goals" is the record of how the first draft hit its wall — read it as history, not instructions.

Ephapax is a research language for principled handling of irreversible boundaries (region exits, drops, key erasure, audit trails) in compile-time-memory-safe WebAssembly. Real systems are irreversible — operating systems deallocate, databases drop tables, security systems erase keys, compilers collapse high-level distinctions. Ephapax is designed to track not just what is owned but what was lost when it was given up, so reclamation can carry evidence where it matters and degrade where it does not. This is a research design goal, not a claim that all language-level soundness obligations are proved.

The core has Coq and Idris2 formal artifacts, but the current Coq preservation story is incomplete and has pinned counterexamples: legacy preservation and the unrestricted L1 statement are false as stated, and no unconditional L2 theorem is established. See the proof ledger and PROOF-NEEDS.adoc before interpreting any local lemma as a language-wide guarantee.

Table of Contents

Why "Ephapax"?
What this is
The four layers
Three superpowers
Design targets and use cases
What this isn’t
Hello, world
Quickstart
Project structure
Formal foundations
- Coq (formal/)
- Idris2 (idris2/src/Ephapax/ + src/formal/)
Surface syntax (locked)
Build targets
Component status
Documentation map
Quickstart files by audience
Seam analysis
Related work
Contributing
Licence
Author

Why "Ephapax"?

The Greek ἐφάπαξ ("ephapax") means once for all. It evokes the linear-typing design goal: track each linear resource so it is consumed exactly once. The intended guarantee must still be established for Ephapax’s judgments, implementation, and operational semantics; current preservation counterexamples show that this is not automatic.

What this is

Ephapax is a programming language with:

Property	What this means
Dyadic discipline (L2)	Each binding is either affine (`let` — used at most once, weakening allowed) or linear (`let!` — used exactly once, weakening forbidden). Type checker enforces. See "The four layers" below for how this composes with L1/L3/L4.
Region-based memory (L1)	Allocations are designed around named regions (`region r: …`). The L1 judgment threads a region-capability environment, but current unrestricted L1 preservation is refuted by pinned Coq counterexamples; sibling safety is a design goal, not an established guarantee. When a region’s scope ends, the runtime bulk-frees resources in it; this implementation behavior is not proved to refine the calculus.
Second-class borrows	`&x` gives temporary access without consuming `x`. Borrows cannot be stored, escape their introduction scope, or be used after the borrowed resource is freed.
Compile-time memory safety (design target)	The intended goal is to reject use-after-free, double-free, and leaks of linear resources before code generation. General preservation and implementation refinement are not established; see `PROOF-NEEDS.adoc`.
WebAssembly target	`wasm32-unknown-unknown` primary; native via Cranelift secondary.
No GC, no allocator runtime	Region exits do the bulk deallocation. No tracing collector, no reference counting, no allocator-per-object metadata.

The four layers

Ephapax’s design separates four disciplines. Their composition and soundness are proof obligations, not an automatic consequence of orthogonality or of a related repository’s theory. echo-types is a conceptual reference; Ephapax-local claims require Ephapax-local proofs.

Layer	What it enforces
L1 — Region capabilities	Region environments are threaded through compound typing rules. This is intended to prevent stale sibling references, but the current preservation statement is refuted as stated by pinned L1 counterexamples; it is not a proved language guarantee. See `PROOF-NEEDS.adoc`.
L2 — Structural discipline (linear ↔ affine)	The modality of the surrounding program decides whether linear bindings must be consumed (Linear: ephapax-linear) or may be dropped (Affine: ephapax-affine). Same syntax, same semantics — different admissible derivations. Linear ⊆ Affine, proved by `linear_to_affine` Qed in `formal/Modality.v`.
L3 — Irreversibility residue (Echo)	Operations that erase information (region exit, drop) produce proof-relevant residue — `Echo f y := Σ A (λ x → f x ≡ y)`. In Linear mode the residue must be observed; in Affine mode it may be silently lowered. Calculus mechanised in `formal/Echo.v`; integration into the typing judgment is the next-block work.
L4 — Dyadic interaction mode	A project-level declaration of which side of the dyad the program speaks from (`ephapax_linear` / `ephapax_affine` / `module_boundary_mix`). Selects the L2 modality and the L3 observation discipline. No proof obligations of its own — mechanical scaffold in `formal/L4.v` carries definitions only by design.

Soundness story

The four-layer separation is a design response to the verified legacy counterexample (formal/Counterexample.v), not itself a soundness proof. Later pinned regressions refute the current unrestricted L1 preservation statement, and no unconditional L2 preservation theorem is established. Making invariants explicit is necessary design work, but every Ephapax typing/step combination still requires a local theorem with proven assumptions. See PROOF-NEEDS.adoc for the current boundary.

Three superpowers

The L3 echo / residue layer (Ephapax’s contribution to the four-layer design) opens three things proper reversible programming struggles with:

Superpower	What it gives you
A. Accountability of irreversible reclamation	The design aims to make irreversible events (`S_Region_Exit`, `S_Drop`) carry typed evidence under Linear discipline, with a more permissive Affine path. This is a design intent; the local L1/L2 preservation gaps mean it is not yet an end-to-end proved guarantee.
B. Selective reversibility (thin-poset)	Linear ≤ Affine is a two-point thin poset at the L2 modality. You pick per-region (or per-project) which discipline applies. Same code shape, different evidence obligations. Concrete examples: Linear during backpropagation (must keep the gradient residue); Affine during inference (drop the residue, save memory). These are design examples; their safety properties require local proofs and are not established by the modality poset alone.
C. Debugging + provenance	The design uses Linear Echoes to require receipts (preimages) for selected state changes and permits opting out in Affine mode. The intended guarantee is that evidence is retained, but current preservation gaps mean this must not be described as a proved end-to-end language guarantee yet.

Caution

Echo Types are NOT a tracing-GC replacement

Echo Types do not solve reachability or cycles. They are not a "fire-and-forget" automatic memory manager. Their strength is accountability of irreversible reclamation in systems that already know when and how to deallocate (regions, explicit drop, deterministic ownership). Treating them as competition for mark-and-sweep or generational GC is a category error.

The committed v1 direction is Linear Echo + Region-Based Memory Management (deterministic bulk free with mandatory certified evidence). A speculative future direction is an optional Linear discipline on deterministic Rust-style drop for critical resources (keys, sensitive buffers requiring provable erasure) — flagged but not committed.

Design targets and use cases

These are intended applications of the design, not currently established end-to-end language guarantees. Any particular safety claim needs a proved Ephapax theorem with its exact assumptions and implementation boundary.

Mandatory evidence for critical actions (design target). A future Linear-echo discipline is intended to require observation of selected region exits or drops. The current L3 Qed lemmas cover matching rule pairs only; they do not establish this end-to-end guarantee.
GDPR "right to be forgotten" with certified evidence of erasure (potential application). The design explores making deletion evidence explicit. No current Ephapax theorem proves erasure, notification, or logging for personal-data programs.
Resource management for keys, secrets, and sensitive buffers (potential application). The design aims to make selected deallocation events auditable; it does not currently prove physical erasure or implementation refinement.
Selective reversibility. The Linear/Affine modality is mechanised, and the Echo calculus has a local non-invertibility result. These isolated facts do not prove the proposed system composes soundly or provides end-to-end guarantees.
Potential foundation for policy enforcement. Any compliance claim requires a precisely scoped Ephapax theorem and an implementation boundary; cross-repository Echo results and conceptual vocabulary do not discharge those obligations.

What this isn’t

Not Rust. Rust uses ownership + borrowing with a single discipline (affine-ish, with linearisation via Drop). Ephapax separates the two disciplines explicitly: let is affine, let! is linear, and the user chooses per-binding.
Not a research vapourware. 17 active Rust workspace crates + tests/fuzz (with src/ephapax-tools/ outside the workspace and src/ephapax-vram-cache/ explicitly disabled — needs hyperpolymath/ephapax-proven); the lexer, parser, interpreter, REPL, CLI, S-expression IR, two-phase pipeline, Zig FFI, and conformance test suite are complete. Type checker and WASM codegen are in progress. See ROADMAP.adoc.
Not yet self-hosting. The compiler is written in Rust. The formalisation is in Coq + Idris2. Self-hosting is a v1.0+ goal.

Hello, world

fn main() -> i32 {
    let x = 1 + 2;
    let y = x * 3;
    y
}

A region with linear strings:

region r:
    let s1 = String.new@r("hello, ")
    let s2 = String.new@r("world")

    -- Borrow s1 to get length (does not consume)
    let len = String.len(&s1)

    -- Concatenation consumes both strings
    let result = String.concat(s1, s2)

    -- result is consumed by being returned
    result
-- Region exits: any remaining allocations bulk-freed.

A linear binding (must consume):

fn process(input: i32) -> i32 {
    let! z = copy(input) in
    z + 1  -- z is consumed exactly once
}

More examples in examples/ and conformance/valid/.

Quickstart

# Build all crates
just build

# Build the Idris2 affine stage
just idris-build

# Verify Coq proofs
just proofs

# Run conformance tests + build + proofs
just golden

# Compile an .eph file through Idris2 + WASM backend
just compile-affine input.eph affine output.wasm

Prerequisites:

Rust 1.83+ with wasm32-unknown-unknown target
Coq 8.18+ (for proof verification)
Idris2 0.8.0 (needs IDRIS2_PREFIX pointing at a prefix with TTCs)
just (task runner)

Project structure

ephapax/
├── formal/                       # Coq syntax, judgments, semantics, lemmas, and counterexamples
│   ├── Syntax.v                  # AST and types
│   ├── Typing.v                  # Region-linear typing rules
│   ├── Semantics.v               # Small-step substitution semantics
│   └── PRESERVATION-HANDOFF.adoc   # Per-case checklist for preservation
├── idris2/                       # Idris2 frontend (parser + typechecker)
│   ├── src/Ephapax/IR/           # AST, decode/encode, S-expression IR
│   ├── src/Ephapax/Parse/        # Lexer, parser, stream, ZigBuffer FFI
│   └── src/Ephapax/Affine/       # Type checker, emitter
├── src/formal/                   # Idris2 region-linearity theorems
│   └── Ephapax/Formal/           # noEscape, regionSafety, noGC, orthogonality
├── src/                          # Rust implementation
│   ├── ephapax-syntax/           # Core AST (Coq-proven shape)
│   ├── ephapax-surface/          # Surface AST (data, match, patterns)
│   ├── ephapax-desugar/          # Surface → Core
│   ├── ephapax-typing/           # Dyadic type checker
│   ├── ephapax-parser/           # Pest PEG parser
│   ├── ephapax-lexer/            # logos tokenizer
│   ├── ephapax-interp/           # Tree-walking interpreter
│   ├── ephapax-wasm/             # WASM code generator
│   ├── ephapax-runtime/          # no_std WASM runtime with regions
│   ├── ephapax-cli/              # CLI
│   ├── ephapax-lsp/              # Language server
│   └── ephapax-analysis/         # Escape / free-vars / liveness analysis
├── ephapax-linear/               # Standalone dual-discipline checker
├── ffi/zig/                      # Zig FFI implementation
├── conformance/                  # Type-system conformance tests
├── spec/                         # Language specification
└── docs/                         # Vision, ADRs, comparisons, reports

Formal foundations

The type system is grounded in:

Intuitionistic linear logic — resource-sensitive reasoning
Separation logic — memory ownership and framing
Tofte-Talpin region calculus — scoped allocation

Two complementary formalisations, both run on every push:

Coq (`formal/`)

Operational semantics with small-step reduction over a substitution- based calculus. Post-2026-05-26 the formalisation is layered:

Legacy (formal/Semantics.v, formal/Typing.v) — the original pre-discovery judgment. Its preservation statement is provably false: it is now preservation_stmt : Prop, refuted by Counterexample.preservation_false (Qed). The former Admitted. was retired on 2026-11-05 (owner-ratified D0/D0b). Do not extend. Treat as archaeology — see STATUS.adoc for the pre-discovery PR list and the explicit do-not-do reasoning.
Layer 1 — region capabilities (formal/TypingL1.v, formal/Semantics_L1.v). The modality-indexed judgment threads a capability environment R. The judgment and helper lemmas are mechanised, but the unrestricted preservation_l1 statement is refuted by Counterexample_PreservationL1.v; its supporting step_pop_disjoint_from_type_l1 statement is separately refuted by Counterexample_StepPop.v. Both are retired to Prop statements (preservation_l1_stmt, step_pop_disjoint_from_type_l1_stmt; D0, 2026-11-05) and are not proof debt. A sound replacement requires a judgment/step redesign and an explicit theorem boundary. See PROOF-NEEDS.adoc.
Layer 2 — structural modality (formal/Modality.v). Linear vs Affine as a K-free thin-poset decoration. linear_to_affine is Qed with zero axioms. Landed via PRs #176 + #177.
Layer 3 — echo / residue (formal/Echo.v). 12 Qed lemmas covering the fiber calculus, degrade map, and the no-section-collapse-to-residue irreversibility theorem (mirrors the upstream Agda development at hyperpolymath/echo-types). Wiring into the L1 typing rules landed via slice 4 (2026-05-27): preservation_l3_region_active_echo, preservation_l3_drop_echo, and the preservation_l3 umbrella are Qed for their matching echo rule pairs; they do not establish general L1/L2 preservation.
Layer 4 — dyadic interaction. Phase A scaffold landed 2026-05-28: formal/L4.v defines ProgramMode (PModeLinear / PModeAffine / PModeBoundaryMix) and the program_mode_to_modality round-trip. No theorems by design (definitions only — labelling discipline, not a proof layer). Design in formal/PRESERVATION-DESIGN.adoc §7.

Per-sublanguage proof debt with explicit do-not-do list lives in PROOF-NEEDS.adoc. The four-layer architecture rationale is in formal/PRESERVATION-DESIGN.adoc. The counterexample itself is formal/Counterexample.v (6 Qed, including preservation_false).

# Verify Coq proofs
just proofs                   # via Makefile.coq
# Or per-file:
cd formal && coqc -Q . Ephapax Semantics.v

Idris2 (`idris2/src/Ephapax/` + `src/formal/`)

Two Idris2 developments:

idris2/src/Ephapax/ — the actual frontend (parser, type checker, IR codec). As of 2026-05-20, the entire layer is under %default total (8 of 9 files) or %default covering (the recursive-descent parser, where fueling 30 mutually-recursive combinators is a deferred separate campaign). Zero assert_total, zero believe_me, zero assert_smaller introduced; 14 covering markers retained for documented Idris2 0.8.0 SCT limits.
src/formal/ — local Idris2 structural results include noEscapeTheorem, orthogonalityLemma, and splitLinearCoverage. regionSafetyExtract and noGCExtract are total but vacuous wrappers returning supplied witnesses. These do not establish operational region safety, general preservation, or Rust/compiler refinement; the ABI obligation register records what remains owed.

# Verify Idris2 frontend total/covering
just idris-build

# Verify Idris2 region-linearity theorems
cd src/formal && idris2 --build ephapax-formal.ipkg

Surface syntax (locked)

// Function declaration
fn main() -> i32 {
    let x = 1 + 2;
    let y = x * 3;
    y
}

// Linear binding
let! z = copy(x) in z

// Region scope
region r:
    let s = String.new@r("data")
    String.len(&s)

Grammar highlights:

Functions: fn name(params) → Ty { … } or fn name(params) : Ty { … }
Affine bindings: let x = expr in expr
Linear bindings: let! x = expr in expr
Block expressions: { expr1; expr2; …; exprN } (final expr is the result)
Newlines are statement separators (equivalent to ;)
Comments: // and -- to end-of-line

Full grammar: spec/ephapax-spec.md. The v2 grammar work (modules, generics, effects, traits, comptime, contracts) lives on feat/v2-grammar-cross-module branches; see GitHub PRs for status.

Build targets

Target	Description	Status
WebAssembly	`wasm32-unknown-unknown`	Primary
Native	Via Cranelift	Secondary

Component status

Component	Status	Notes
Core type-system design (affine + linear)	✅ Complete	Locked in `formal/Typing.v`
Lexer (logos)	✅ Complete
Parser (chumsky + Pest)	✅ Complete
Interpreter (tree-walking)	✅ Complete	Environment-leak fix applied 2026-03-28
REPL	✅ Complete
CLI (`ephapax-cli`)	✅ Complete
Idris2 frontend (S-expression IR)	✅ Complete (`%default total` 8/9)	Parser is `covering`; total upgrade deferred
Type checker (`ephapax-typing`)	🚧 In progress
WASM code generation	🚧 In progress	Lambda/app closure conversion landed; some pair/sum cases use `i32` placeholder representation
Conformance test suite	✅ Complete	Pass/fail cases; covers dyadic discipline
Coq `no_leaks` + region lemmas	✅ Qed
Coq legacy `preservation`	🛑 Retired to `preservation_stmt : Prop` — provably false	Refuted by `Counterexample.preservation_false` (Qed, closed under the global context). Not closable. Archaeology.
Coq L1 (region capabilities)	Judgment and helpers mechanised; unrestricted preservation refuted	`Counterexample_StepPop.v` refutes `step_pop_disjoint_from_type_l1`; `Counterexample_PreservationL1.v` refutes `preservation_l1`. These are pinned regressions, not ordinary open proof debt.
Coq L2 (modality)	✅ Modality core landed (PRs #176 + #177); 0 axioms	`linear_to_affine` Qed. No unconditional `preservation_l2` theorem is established. The L2 β-case lemmas are conditional; `Counterexample_L2.v` and `Counterexample_L2_nested.v` document distinct gaps.
Coq L3 (echo / residue calculus)	✅ Scoped matching-rule preservation results Qed; 0 admits in `Echo.v`	`preservation_l3` and its two case lemmas cover matching echo-emitting rule pairs only; they do not establish general L1/L2 preservation. 12 Qed in `Echo.v` for the underlying calculus.
Coq L4 (dyadic interaction)	✅ Phase A scaffold landed (`formal/L4.v`, 2026-05-28); definitions only	`PModeLinear` / `PModeAffine` / `PModeBoundaryMix` + `program_mode_to_modality` round-trip. No theorems by design; design in `formal/PRESERVATION-DESIGN.adoc §7`.
Idris2 structural results	✅ Local total proofs; two extraction wrappers are vacuous	`noEscapeTheorem`, `orthogonalityLemma`, `splitLinearCoverage`, and `outlivesTransitive` have exact local scopes. No runtime no-escape, general language soundness, or implementation-refinement proof is established; see the EXPLAINME ledger and `PROOF-NEEDS.adoc` §5.3.
LSP server	🟡 Partial	Basic diagnostics; completion in progress
Standard library	🔲 Planned	`ephapax-stdlib` skeleton exists

Documentation map

Document	What it covers
README	You are here. Overview + quickstart.
STATUS.adoc	Past / present / future map. Single page that answers "where are we?" Read this before any `.v` file or any PR comment dated before 2026-05-26.
PROOF-NEEDS.adoc	Per-sublanguage proof debt audit. What’s done (Qed), what’s todo, what’s banned (anti-pattern detector). Separated for ephapax-linear and ephapax-affine sublanguages.
formal/PRESERVATION-DESIGN.adoc	Design history and architecture. Why the legacy counterexample motivated the four-layer proposal; not proof that preservation holds per layer.
formal/Counterexample.v	The 6 Qed lemmas, including `preservation_false`, that pin the soundness gap of the legacy judgment. Authoritative source of the gap; future proofs must coexist with it.
CLAUDE.md	Agent guidance. Carries the 2026-05-27 owner directive, anti-pattern detector, escalation rule.
EXPLAINME.adoc	"Show me the receipts" — every claim in this README backed by a specific file, test, or proof.
ROADMAP.adoc	Milestones (v0.1.0 → v1.0.0), per-version checklists, current open work. Note: any pre-2026-05-26 closure-plan content is superseded by STATUS.adoc + PRESERVATION-DESIGN.adoc.
formal/PRESERVATION-HANDOFF.adoc	Archaeology only — historical diagnostic record of the pre-counterexample closure attempts. Reads as a closure plan; isn’t one. Useful only for understanding why the redesign happened.
RUST-SPARK-STANCE.adoc	Stance on Rust + SPARK interop and where Ephapax fits.
TOPOLOGY.adoc	Module dependency graph + crate layering.
TEST-NEEDS.adoc	Outstanding test coverage gaps.
CHANGELOG.adoc	Per-release change log.
docs/vision/EPHAPAX-VISION.adoc	Design rationale — why dyadic, why regions, why WASM.
docs/specs/DESIGN-DECISIONS.adoc	17 architecture decision records with rationale.
docs/specs/LANGUAGE-COMPARISON.adoc	Comparison against 10 other languages on the linear/affine axis.
spec/	Language specification + grammar EBNF.
.github/CONTRIBUTING.md	Contribution guide.
CODE_OF_CONDUCT.adoc	Code of conduct.
SECURITY.adoc	Security policy.

Quickstart files by audience

Audience	Start here
End user (just want to compile `.eph` files)	QUICKSTART-USER.adoc
Developer (extending the compiler / language)	QUICKSTART-DEV.adoc
Maintainer (release / governance)	QUICKSTART-MAINTAINER.adoc
Outside observer (what is this even?)	Read this README → `EXPLAINME.adoc` → `docs/vision/EPHAPAX-VISION.adoc`

Seam analysis

Key interfaces where correctness and stability matter:

Idris2 → S-expression IR (Ephapax.IR.Decode encoding/decoding)
Zig FFI token buffer → Idris2 parser stream (Ephapax.Parse.ZigBuffer)
S-expression IR → Rust/WASM backend (ephapax-ir and ephapax-wasm)
Surface AST → Core AST (ephapax-desugar — proofs target core only)

The proven library is a dependency so string-handling paths over the IR boundary harden over time (JSON-style escaping, etc.).

Rust — ownership and borrowing
Linear Haskell — linear types in GHC
MLKit — region-based memory management
Cyclone — safe C dialect with regions
Granule — graded modal types with linear/affine ledger
Tofte-Talpin 1997 — region calculus original paper

docs/specs/LANGUAGE-COMPARISON.adoc has a feature-by-feature comparison against ten of these.

Contributing

Contributions welcome. Please see:

.github/CONTRIBUTING.md — getting started
CODE_OF_CONDUCT.adoc — community standards

The highest-leverage open work, in priority order:

L1/L2 soundness redesign — specify judgment and operational invariants that reject the pinned counterexamples, then state and prove replacement preservation theorems with explicit hypotheses. Existing Phase 3b work is conditional infrastructure, not an unconditional L2 theorem.
Progress for redesigned judgments — state and prove progress and canonical forms only against the final redesigned judgments. Do not combine these with the refuted unrestricted preservation_l1 claim to assert conventional type soundness.
Fuel-refactor Parse/Parser.idr from %default covering to %default total. Substantial — ~30 mutually-recursive combinators threaded through a Stream record.
Type-checker completion (ephapax-typing) and WASM codegen for lambda/app (ephapax-wasm).
Native backend via Cranelift (v0.2.0).

Note

Proving the legacy preservation statement in formal/Semantics.v is NOT a valid contribution. It is provably false: it is retired to preservation_stmt : Prop and refuted by Counterexample.preservation_false (owner directive 2026-05-27; retirement owner-ratified as D0/D0b on 2026-11-05). formal/PRESERVATION-HANDOFF.adoc is archaeology kept for context. The redesigned judgments are a separate development, not yet a sound replacement: preservation_l1 is refuted as stated, and no unconditional preservation_l2 theorem exists. L2 β-case lemmas have explicit preconditions; L3 results cover only matching echo rule pairs. The active work is to specify and prove sound replacement theorems without weakening the pinned regressions. See formal/PRESERVATION-DESIGN.adoc and PROOF-NEEDS.adoc.

Licence

Code is MPL-2.0 — see MPL-2.0.txt.

Documentation is CC-BY-SA-4.0 — see CC-BY-SA-4.0.txt.

Every file carries its own SPDX-License-Identifier: header, so the applicable licence is always the one named in the file itself.

Author

Jonathan D.A. Jewell

"Once for all" — every resource used exactly once.

Navigation Menu

Repository navigation

README.adoc

README.adoc

Ephapax

Why "Ephapax"?

What this is

The four layers

Three superpowers

Design targets and use cases

What this isn’t

Hello, world

Quickstart

Project structure

Formal foundations

Coq (`formal/`)

Idris2 (`idris2/src/Ephapax/` + `src/formal/`)

Surface syntax (locked)

Build targets

Component status

Documentation map

Quickstart files by audience

Seam analysis

Contributing

Licence

Author

FilesExpand file tree

README.adoc

Latest commit

History

README.adoc

File metadata and controls

Ephapax

Why "Ephapax"?

What this is

The four layers

Three superpowers

Design targets and use cases

What this isn’t

Hello, world

Quickstart

Project structure

Formal foundations

Coq (formal/)

Idris2 (idris2/src/Ephapax/ + src/formal/)

Surface syntax (locked)

Build targets

Component status

Documentation map

Quickstart files by audience

Seam analysis

Related work

Contributing

Licence

Author

Coq (`formal/`)

Idris2 (`idris2/src/Ephapax/` + `src/formal/`)