 Let us also report on progress on the methodological issues the finitist consistency program was to address. First of all, due to quite a bit of important historical work, we have a much better grasp of the evolution of the program in the 1920s and its roots in the development toward modern structuralist mathematics in the nineteenth century. The work of editing Hilbert’s unpublished lecture notes has opened a treasure of  information.[32]  The connections to the development in nineteenth century mathematics are hinted at in  Appendix A,  but they are explored in greater depth, for example, in Ferreirós 2008; Reck 2003, 2013; and the papers Sieg wrote on Dedekind with Morris (forthcoming) and Schlimm (2005, 2017), respectively. Secondly, as to the properly methodological issues, we presented some broad considerations in  section 4.1,  namely, that consistency proofs should be given relative to “constructive” theories. We did not make any remarks about what is characteristic of a constructive perspective and why such a perspective has not only a mathematical, but also a philosophical point. There is, of course, a very rich literature. Let us point to some informative sources: van Atten (2007) as defending Brouwer’s views, Martin-Löf (1984) as exposing the philosophical motivation for his type theory, Feferman (1988, 2000) discussing the foundational point of proof theory, Bernays (1976) as presenting crucial aspects of an informed philosophy of mathematics, and (Sieg 2013) as explicating (the context for) his reductive structuralism.