A partial realisation of Hilbert’s programme in (commutative) algebra has proved practicable in the preceding years. It means to exclusively work with finite methods, and without ideal objects such as prime ideals, whenever the data under consideration are sufficiently concrete. In other words, constructive proofs are sought, and found, during which one need not go beyond the type level on which the theorems are formulated. This approach of a point-free and syntactical flavour gained power when ideas from formal topology and from dynamical algebra were combined. As stressed by Wraith, its success is guaranteed by Barr’s completeness theorem for geometric logic, in which large parts of algebra can be formulated.

One of the milestones was the elementary and inductive characterisation of Krull dimension given by Coquand, Lombardi, and Roy. This made possible, among other things, a constructive proof on low type levels of the theorem of Eisenbud-Evans-Storch, which says that d+1 polynomials suffice to generate, up to radicals, any finitely generated ideal of univariate polynomials with coefficients in a ring of Krull dimension d. (This generalises the fact that every variety in dimension d is an intersection of d hypersurfaces, for which Kronecker still needed d+1 hypersurfaces.)

As a typical theorem with concrete input and concrete output, the Eisenbud-Evans-Storch theorem merits a proof exclusively done by finite methods. The proof we have produced with Coquand and Lombardi further provided deeper insight into the topological character of the problem, and prompted a variant of Kaplansky’s regular element property which is of some interest on its own. We take this theorem and its proof as a guiding example for our survey, and will indicate some possible future work.