A "proof" of a general arithmetic proposition is a function which yields for each argument a proof of that instance of the
general proposition.
But of course, simply presenting such a function (even if that weren't in the present context itself problematic) does not
constitue a proof (for if it were, as he observes, a proof of the consistency of ZF would be readily forthcoming).
You have of course to "prove" in some other sense, that this function does what it is supposed to do.
The "propositions as types" enthusiasts appear at first sight to be offering a radical new notion of proof to replace the
one we had, but we find that these proofs are not checkable, they are not decidable.
You have to have an old fashioned proof to establish that you have one of the new proofs.

So it immediately seems to me that Tait is immersed in problems which have not been connected with finitism and which seem
to be entirely a product of his introduction of constructive proof methods.

So I left the chapter in frustration and looked around at what else was in the book, eventually returning to read the second
of his two chapters on finitism.
Here I noticed in the next paper a reference to Zach's PhD thesis, which seemed a good place to look for a clearer picture
of what Hilbert's finitism was.

I downloaded Zach's thesis, which was very helpful, and quickly got a slightly better understanding of finitism, including
that it was a part of Hilbert's conception of finitist proof that the proof of a generalisation would involve exhibiting a
function which from any object in the domain of discourse (the numbers) would contruct a proof of the instantiation of the
generalisation to that object.
OK, so we don't actually have "propositions as types", but we do have a very constructive notion of proof, and perhaps the
connection between this and infinity is accepted from Brouwer.

Generally, Tait has launched into his account of finitism in a way which is very bound up with more modern constructivist
ideas, and the result is that it is completely unclear to me which of the problems which he is addressing are really inherent
in finitism and which are merely problems in the constructive machinery with which he is attempting to give an account of
finitism.