 Moreover, he was aware that the incompleteness theorems are a price that has to be paid for communicating and verifying proofs in a sufficiently strong formalized language that also meets his requirement of effectiveness (discussed in  §2).  The theorems, their significance for Hilbert’s program, their relation to effectiveness, and their relation to Tarski’s work are discussed in some detail in chapter VIII of Church’s textbook on mathematical logic (1968/1972/1976; printed in BE). Here Church also acknowledged the value of Gentzen’s and Gödel’s consistency proofs, but apparently did not think their significance was “major”. A finitary consistency proof in the sense of Hilbert was desirable but impossible.