Effectful Software Contracts
summary
Presents a formal design that lets contracts perform effects while proving they do not change successful runs: an erasure theorem showing contract checks cannot unduly interfere with program execution. Uses effect handlers to separate contract-effect handlers from main handlers, imposes a restrictive single-use/linear continuation discipline, and proves blame correctness. Ships a faithful Hashlang implementation plus a Rackety backward-compatible version and evaluates by reimplementing several prior effectful-contract examples (bounded-use, stateful checks); restrictions are tight but the prototypes work and artifacts are available.
AI-written summary · about
chapters (8)
- 0:00Effectful software contracts
- 2:59Contracts with intentional effects
- 5:50Formalizing effect usage
- 7:36Effect handlers in contracts
- 10:06Bounded-use function contracts
- 13:21Handling effects with handlers
- 15:05Theory and implementations summary
- 16:32Q&A on verification
related talks
15mEffects as Capabilities: Effect Handlers and Lightweight Effect Polymorphism
15mHandling Bidirectional Control Flow
51mEffects: to be or not to be?
25mA Relational Separation Logic for Effect Handlers
27mLimiting side-effects of applications at compile-time
15mZero-Overhead Lexical Effect Handlers
15mEffect Handlers, Evidently
15mEfficient Compilation of Algebraic Effect Handlers