That's essentially correct. Extraction is a term in roqc. A rocq program contains both a computational part, and proofs about that computation, all mixed together in the type system. Extraction is the automated process of discarding the proofs and writing out the computational component to a more conventional (and probably more efficient) programming language.
The original extractor was to ocaml, and this is a new extractor to c++.
Is early termination the only supported side effect? Its name suggests a more general capability, but I didn't see more examples in my (cursory) look at the readme
Early termination is the most common use case, but it’s not the only thing SideEffect represents.
The name is intentionally a bit broader — it’s meant to model “effects where normal composition should stop”.
In practice, that includes things like validation failures, logging or notifications at pipeline boundaries, and error reporting or metrics.
That said, the scope is deliberately conservative.
SideEffect isn’t meant to be a general-purpose effect system.
If it were, it would quickly turn into something very close to a monad or effect framework, which I’m intentionally avoiding.
Not saying if the title is good or bad, but just to provide context: there's a tradition of these style of apple-language explainers / cheat sheets titled in this pattern. First I'm aware of is https://fuckingblocksyntax.com/ . There seem to be at least 15 of them listed on https://fuckingsyntaxsite.com/ , and probably more with different swears. It's a genre of titles in the same vein as "considered harmful" or "falsehoods programmers believe about"
My recollection was the block syntax one being first as well, back when that was added to Objective-C. It was arcane enough to have to look up all the time.
reply