Many mathematicians seem to have an attitude that a well peer-reviewed proof is simply correct and etched in stone for good. This seems to me like publishing programs - some of them thousands of lines long - and expecting them to be essentially bug-free without ever running them.

Von Neumann is not exactly making the same point, but he is arguing against the sense that math is a kind of purely abstract discovery that has escaped from the messiness of day-to-day reality.

One could ask: will we ever get to a point when all mathematical proofs are rigorously checked, so that we know they're correct? I hope we do get to a point when program-checked proofs are standard, but even then there's the possibility that a proof-checker itself is buggy. So, philosophically, it seems we may never justifiably feel certain beyond all doubt that any given proof is correct.

But we can have greater confidence in a proof verified by both expert humans and by a trusted program than in a proof simply reviewed by humans. So the effort is meaningful and worthwhile - all in the context of seeing math as a field as fallible as any other.