Bond (Design by Contract for Elixir) - 1.3.0 released: contract inheritance & refinement

jvoegele · June 15, 2026, 8:28pm

For anyone curious about future directions for Bond, I’ve created some forward-looking issues in GitHub issue tracker:

Future directions for Bond (post-1.3.0)

opened 07:10PM - 15 Jun 26 UTC

enhancement

Tracking issue for post-1.3.0 feature exploration, grouped the way #11 grouped t…he road-to-1.0 work and #17 grouped contract inheritance. None of these are committed or scheduled — this captures the design space while it's fresh. **Context:** As of 1.3.0, Bond implements essentially the entire core Eiffel contract model (`@pre`/`@post`, struct `@invariant`, `old`, `result`, `check`, conditional compilation) plus contract inheritance for behaviours and protocols (#17) and Eiffel-style refinement `@pre_weaken`/`@post_strengthen` (#16). The remaining ideas split into classic-DbC gaps and Elixir-native directions. ## Candidate features (issues filed) - [x] #32 — **Quantified assertions** (`forall`/`exists`) with element-level diagnostics. *Best value-per-effort; plays to Bond's precise-message strength.* - [ ] #33 — **Failure contracts** (`signals`-style): constrain which exceptions a function may raise. - [x] #34 — **Stateful process / GenServer contracts**: state invariants + history constraints. *Highest ceiling — uniquely Elixir; likely its own epic.* - [x] #35 — **Reusable, named contracts**: share `@pre`/`@post` across functions. *User-requested (the @Petr thread).* - [ ] #36 — **Contract-driven test generation**: boundary probing + ExUnit derivation (à la Eiffel AutoTest). ## Recommended starting points - Quickest wins: **#32** and **#35** (small, low-risk, shippable as minors; #35 is user-validated). - Biggest opportunity: **#34** (DbC for the actor model — doesn't exist elsewhere). ## Considered but deferred (poor fit / low value — not filed) - **Loop / recursion variants** (Eiffel `variant`, for termination): no loops in Elixir; a recursion-variant analog is niche and awkward to attach to arbitrary recursion. - **Frame conditions** (Eiffel `only`, JML `assignable`, Dafny `modifies`): nothing to frame in an immutable language at the data level. The only meaningful place is process/ETS state — folded into #34. - **Invariant inheritance / behaviour-level invariants** (Eiffel conjoins invariants down the hierarchy): structs don't inherit; weak fit. (Deliberately excluded from #16 for the same reason.) - **Purity enforcement for assertion helpers** (Eiffel CQS, JML `pure`): hard to determine purity in Elixir; a lint warning at most, low value. ## Explicitly out of scope Static verification / formal proof (SPARK, Dafny) and ghost/model fields — theorem proving, not runtime checking. Bond's lane is runtime checks that complement typespecs and ExUnit, and that boundary is intentional. _Captured from a design discussion (post-1.3.0)._