I'd agree with the author that only logicians are interested in formal proofs.
But what the author describes as the Hilbet-Bourbaki method is simply what math is. Any mathematician will tell you that if you're not proving theorems then you're not really doing math.
Anyway, what good is a computer proof if it doesn't provide any insight ? (which is usually the case). A good proof usually illuminates why some mathematical statement is true, and that is why computer proofs are usually looked upon with suspicion by many mathematicians.
After all, a computer simply churning out the answer (42 ?) doesn't advance the state of human knowledge at all.
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.
He isn't disagreeing with the goals of math as practiced. All your quotes illustrate is that he thinks the usual methods are woefully inefficient.
More quotes:
"and I believe that mathematicians who continue to do pure human, pencil-and-paper, computer-less, research, are wasting their time." If they learned how to program, in, say, Maple, and used the same mental energy and ingenuity while trying to use the full potential of the computer, they would go much further.
I.e., human + computer >> human.
"The axiomatic method is not even the most efficient way to prove theorems in Euclidean Geometry." Thanks to Rene Descartes, every theorem in Euclidean Geometry is equivalent to a routine identity in high-school algebra,
I.e., verifying algebraic identities is easier than euclidean proofs, especially if done by maple.
His main argument is simply that computer-assisted proofs should not be held to a higher standard than human-only proofs.
"I.e., verifying algebraic identities is easier than euclidean proofs, especially if done by maple."
If something like that has been discovered, fine, use it, and solve geometry problems in that way in the future. But how would that have been discovered without doing classical mathematical proofs? I don't think that some problems can be solved algorithmically proves that the same holds for all problems.
He isn't arguing against classical mathematical proofs. He is arguing that informal computer assisted proofs should not be held to a higher standard than informal human created proofs.
Brokers don't trade with their own money, they trade on behalf of clients.
They make a living by charging their clients a small commission for making the trade. Brokers make money when the market is going up, and they make when money the market is going down.
You might like to follow up with this:
http://wangafu.net/~nickm/libevent-book/01_intro.html
Which is the introduction to this:
http://wangafu.net/~nickm/libevent-book/TOC.html