Two methods exist for extracting computational content from classical proofs. Herbrand schemes use higher-order recursion schemes to extract Herbrand disjunctions — finite sets of witnesses that together cover all cases of an existential statement. Functional interpretation, due to Gödel and extended by Gerhardy and Kohlenbach, extracts witnessing functionals through a systematic translation of logical connectives into functional types.
Enqvist-Pyk shows these are the same thing.
Herbrand schemes, reformulated in the right language, become a functional interpretation of classical sequent calculus. The extraction of witnesses via recursion schemes and the extraction via functional translation produce the same computational objects through the same structural mechanisms, just described in different formalisms.
The connection is not approximate. The reformulation preserves the essential feature of Herbrand schemes — they work without cut elimination. Standard proof-theoretic approaches to extracting computational content require eliminating cuts (detours through lemmas) from proofs first, an exponentially expensive transformation. Herbrand schemes bypass this by working directly on the sequent calculus proof with cuts intact.
The functional interpretation inherits this property. The unified view shows that Gerhardy-Kohlenbach functional interpretation and Herbrand extraction are two descriptions of the same proof-theoretic operation, one in the language of type theory and one in the language of recursion schemes.
Two research communities, two formalisms, two sets of theorems about extracting programs from proofs. One operation.