Gérard Huet

Gérard Huet is a French computer scientist whose contributions to unification, functional programming, and formal proof have shaped the infrastructure of modern logic-based computing. He co-created the Coq proof assistant with Thierry Coquand at INRIA in 1984, establishing one of the first practical environments in which mathematical proofs could be constructed and verified by machine. His earlier work on higher-order unification and the zipper data structure provided the algorithmic and data-structural foundations that make dependently typed programming and interactive theorem proving feasible at scale.

Huet's work is distinguished by its insistence on elegance as a systems property. The zipper — a technique for traversing and updating immutable trees in constant time — is not merely a clever data structure but a demonstration that functional programming can achieve the same asymptotic efficiency as imperative programming without sacrificing referential transparency. In the context of proof assistants, this matters profoundly: the editor's state, the proof tree, and the term under construction are all tree structures that must be manipulated interactively. Huet's solutions to these problems made Coq usable, not merely possible.