What the author is disagreeing with, the Hilbert-Bourbaki method, isn't mathematics as the proving of theorems, but rather the proving of theorems as a necessarily formal task; that is, that when one is doing a proof it ought to be done in a (preferably intuitionistic) formal system with no steps omitted. The alternative, and what almost all mathematicians do in practice, is to informally lay out a proof that any professional mathematician (but, perhaps not a computer) can follow, filling in details as necessary.
Further, formal computer proofs are rarely wholly generated by computer. Rather the user specifies goals and tactics which the computer verifies or refutes. If one is using a reasonably powerful logic (ie first-order and not propositional) there are only relatively small tasks that can be automated. Hence, the result is often equivalent, or, at least, close to a human generated proof in terms of what is illuminated about the mathematical statement, but every step is necessarily valid.
Further, there is a field of modern mathematical logic called proof mining which concerns itself with the analysis of fully formal proofs and can often obtain illuminating details from a formal proof that wouldn't be possible from an informal equivalent.
This isn't to say that all mathematics should be formal in the sense indicated, but just to point out that it remains an interesting endeavor that is worth keeping an eye on. Also, note that the author /does/ think that formal verification of this sort can be useful for software development which is indeed what formal methods are mostly used for these days.
Further, formal computer proofs are rarely wholly generated by computer. Rather the user specifies goals and tactics which the computer verifies or refutes. If one is using a reasonably powerful logic (ie first-order and not propositional) there are only relatively small tasks that can be automated. Hence, the result is often equivalent, or, at least, close to a human generated proof in terms of what is illuminated about the mathematical statement, but every step is necessarily valid.
Further, there is a field of modern mathematical logic called proof mining which concerns itself with the analysis of fully formal proofs and can often obtain illuminating details from a formal proof that wouldn't be possible from an informal equivalent.
This isn't to say that all mathematics should be formal in the sense indicated, but just to point out that it remains an interesting endeavor that is worth keeping an eye on. Also, note that the author /does/ think that formal verification of this sort can be useful for software development which is indeed what formal methods are mostly used for these days.