Hi folks! Today I’d like to share a new experiment of mine: Hoop, an algebraic effects and handlers library for PureScript whose runtime core is implemented and verified in F*.
Overview
Hoop is a library for algebraic effects and handlers.
It is not production-ready yet. Nevertheless, I think it provides an interesting demonstration of a new methodology for implementing high-assurance PureScript libraries—particularly libraries that require a substantial foreign runtime.
Unlike purescript-run, Hoop does not represent its computations in PureScript using typed free-monadic machinery such as purescript-free. Instead, it ships with a foreign runtime whose internal computation tree has a freer-monad-like structure, hidden behind the PureScript API.
A CEK-like abstract machine evaluates this computation tree using an explicit stack of defunctionalized continuation frames and eventually produces a result. This is similar in spirit to the approach used by purescript-aff, where an Aff computation is executed by a trampolined interpreter loop.
A Formally Verified Runtime Core
The most distinctive part of this experiment is the use of a theorem prover in the implementation of the effect runtime.
PureScript has a remarkably expressive type system. However, the correctness of foreign modules—usually written in JavaScript—ultimately depends on developer discipline. The larger and more complex a foreign module becomes, the larger the portion of the program that lies outside the guarantees provided by PureScript’s type system.
Traditionally, we have mitigated this risk through testing. Tests are indispensable, but they can demonstrate the presence of bugs, not their absence: they examine selected executions rather than every possible execution.
I therefore implemented the core runtime in F* instead of writing it directly in JavaScript. F* is a proof-oriented functional programming language with dependent and refinement types. Like systems such as Rocq, Agda and Lean, it allows programs and machine-checked proofs about those programs to coexist.
The F* implementation is extracted to OCaml, compiled to JavaScript using js_of_ocaml, and then imported from PureScript through the FFI:
F* source and proofs
↓ extraction
OCaml
↓ js_of_ocaml
JavaScript
↑ foreign import
PureScript
Effect systems and operational semantics have been studied extensively in programming-language theory, which makes their essential structures comparatively amenable to formalization.
At present, Hoop supports first-order algebraic effects. I have proved, among other things, the following properties of its runtime:
-
Correct handler lookup and continuation capture. Handler lookup selects the innermost matching prompt. The captured and remaining stack segments partition the original stack without dropping or rearranging frames, and the captured segment includes the selected prompt, giving Hoop deep-handler semantics.
-
Correct transition rules. The F* implementation of each machine transition agrees with its intended small-step rule, including
perform, handler installation, value return, and continuation resumption. -
The monad laws, up to observational equivalence. Left identity holds unconditionally. Right identity and associativity hold under an explicit congruence assumption about the clause interpreter at the FFI boundary.
-
Algebraicity of effect operations. A performed operation commutes with subsequent monadic binding, under the same congruence assumption. Conversely, a concrete counterexample demonstrates that
Handleneed not be algebraic—which is expected, since it is a handler-forming construct rather than an effect operation. -
Runtime soundness. Provided that a program is well scoped—meaning that it performs only operations available in its current handler context—and that the foreign clause dispatcher preserves well-scopedness, the machine never reaches
Stuckbecause of an unhandled operation.
The final result is a partial-correctness theorem. Hoop is Turing-complete, so termination is neither claimed nor generally provable. Instead, the theorem states that the machine may diverge, but if it returns, it returns a value rather than getting stuck on an unhandled operation.
That last theorem is particularly important: it turns the abstract invariant of well-scopedness into a concrete safety property of the runtime machine.
These main results are supported by well over fifty additional definitions and lemmas concerning stack partitioning, handler lookup, preservation, progress, observational equivalence, and multi-step execution.
The Boundary of Trust
It is important to be explicit about what has—and has not—been verified.
The proofs concern the F* implementation and its formal model. Transferring those guarantees to the shipped JavaScript requires trusting several components:
- the F* implementation and extraction pipeline;
- the OCaml compiler;
-
js_of_ocaml; - the handwritten OCaml/JavaScript FFI boundary, currently about 270 lines, which uses unchecked identity coercions for opaque JavaScript values; and
- the assumption that the typed PureScript API and the foreign clause dispatcher satisfy the well-scopedness and congruence conditions required by the theorems.
In particular, the connection between PureScript’s effect-row types and the F* well-scopedness predicate has not yet been mechanized end to end.
For this reason, I still maintain tests at the F*, PureScript, and generated-JavaScript levels. The proofs establish universal properties of the formalized algorithm, while the tests help detect mistakes in the trusted integration and compilation pipeline.
Future Work
There is also an important distinction between proving metatheoretic properties of the machine and proving that the machine implements the intended semantics.
The current results establish properties of Hoop’s operational semantics: preservation, progress, monad laws, algebraicity, and related invariants. They do not, by themselves, prove that every user-visible behavior agrees with an independent mathematical specification of algebraic effects.
A natural next step would therefore be to define a denotational or other reference semantics and prove an adequacy or correctness theorem relating it to the operational machine.
On the feature side, I plan to work on:
- integrating evidence passing into the runtime’s dispatch path;
- parameterized or parametric handlers;
- higher-order and scoped effects;
- optimized support for tail-resumptive clauses;
- benchmarks, API stabilization, and broader ecosystem testing.
If these pieces come together, I hope Hoop can grow from a verification experiment into a genuinely practical algebraic-effects library for PureScript.
