Leroy traces control from goto to algebraic effects

Xavier Leroy’s preview of Control structures in programming languages: from goto to algebraic effects gives programmers a map of control flow from goto to effect handlers. Cambridge University Press plans to publish the book, and Leroy has released an HTML preview with code samples.

Thesis

Leroy treats control structures as the machinery that lets programmers direct execution. He starts with jumps and structured programming, then moves through coroutines, continuations, exceptions, monads, algebraic effects, and proof methods.

That arc matters because programmers use control operators to shape APIs, schedulers, parsers, error handling, backtracking, and concurrency. A language’s control model decides which patterns feel natural and which patterns demand ceremony.

Key arguments

Leroy links imperative and functional traditions through one question: who controls the next step of execution? In a loop, the programmer controls repetition. In an iterator, the consumer and producer share control. In a continuation, the program reifies the future of a computation. In an effect handler, the programmer captures an operation, decides how to handle it, and resumes or stops the computation.

The table of contents shows a careful climb. Part I covers imperative control structures, including structured programming, non-local control, and control inversion. Part II moves into functional languages, continuations, CPS transformation, and control operators. Part III connects exceptions, user-defined effects, monads, and algebraic effects. Part IV turns to reasoning, with type-and-effect systems, Hoare logic, and separation logic.

Leroy’s background gives the project weight. His work on OCaml and the CompCert verified compiler ties language design to proof, implementation, and long-term maintenance. The book preview also connects with his Collège de France course, Control structures, which frames control as a concept programmers can manipulate.

Implications

Programmers who know exceptions and async code can use algebraic effects as a broader lens. An effect marks an operation such as failure, choice, state, or suspension. A handler decides the policy. That split lets a library expose operations without baking in one execution strategy.

Language designers gain a shared vocabulary for features that often look separate. Generators, coroutines, exceptions, and delimited continuations all deal with captured control. Algebraic effects give researchers and implementers a way to discuss those features with types and laws attached.

The proof chapters signal a second audience: engineers who need confidence in compilers, runtimes, and program transformations. Control flow complicates reasoning because jumps, handlers, and continuations change the shape of execution. Leroy brings Hoare logic and separation logic into the discussion so readers can see how proof techniques adapt.

Counter-perspectives

Algebraic effects still ask a lot from language users. A handler system can make code more modular, but it can also hide execution paths from readers who expect direct calls and returns. Tooling, stack traces, and mental models need to keep pace.

Monads also retain appeal because they make effects explicit in types and APIs. Some teams may prefer that discipline, even if it adds surface syntax. Others may choose handlers because they want direct-style code with stronger abstraction.

Leroy’s book preview suggests a useful standard for the debate: judge a control feature by the programs it clarifies and the reasoning it supports. Syntax matters, but execution and proof decide whether a feature earns its place.