Proof and software
How well accepted are proofs where critical parts depend on software of which we have no access to the source, e.g Mathematica, Maple?
More generally how much can we take on faith with regards to software. Do we have to check the compiler for the Four Color Theorem?
A few years ago the Notices of the American Mathematical Society ran a series of articles on the state of the art in using computer proof assistants. They are at least worth skimming.
"Formal Proof," by Thomas Hales
"Formal Proof - The Four-Color Theorem," by Georges Gonthier
"Formal Proof - Theory and Practice," by John Harrison
"Formal Proof - Getting Started," by Freek Wiedijk
I tend to be a traditionalist when it comes to traditional methods versus computer methods, but I do find arguments like the following compelling.
(This is from a news release from the AMS on their series of articles on formal proof.)
"When mathematicians prove theorems in the traditional way, they present the argument in narrative form. They assume previous results, they gloss over details they think other experts will understand, they take shortcuts to make the presentation less tedious, they appeal to intuition, etc. The correctness of the arguments is determined by the scrutiny of other mathematicians, in informal discussions, in lectures, or in journals. It is sobering to realize that the means by which mathematical results are verified is essentially a social process and is thus fallible." [emphasis mine]
(And this is from Hales's article.)
"The computer code that implements the axioms and rules of inference is referred to as the kernel of the system. It takes fewer than 500 lines of computer code to implement the kernel of HOL Light."
Verifying correctness on such a small program would be a lot easier than verifying correctness of proofs of many theorems.
(Also from Hales's article.)
"Experience from other top-tier theorem-proving systems has been that about three to five bugs have been found in each system over a period of 15-20 years of use. After decades of use on many different systems, to my knowledge, only one proof has ever had to be retracted as a result of a bug in a theorem-proving system, and this in a system that I do not rank in the top tier... We can assert with utmost confidence that the error rates of top-tier theorem proving systems are orders of magnitude lower than error rates in the most prestigious mathematical journals." [emphasis mine again]
As a side note, Hales's paper also lists several major theorems (already proved the traditional way, of course) that have been since proved by a computer. These include quadratic reciprocity, the prime number theorem, the fundamental theorems of algebra and calculus, the Jordan curve theorem, and the Brouwer fixed-point theorem.
Besides the Four-Color Theorem, apparently the Robbins conjecture was first proved by an automated theorem prover.
And, of course, there's Wikipedia on computer-assisted proof.
Many of your questions are adressed in this new book of Jon Borwein and Keith Devlin:
http://books.google.de/books?id=B8Crn_VF9RoC&lpg=PP1&ots=0FLkjZPQ2T&dq=the%20computer%20as%20crucible&hl=en&pg=PP1#v=onepage&q&f=false
I'd argue for a mixed proof system. Computer proofs should be more accepted that they are now, but the tradition is slow to build. I'd rather trust a proof that has also been checked by a computer, in addition to traditional peer-review. After all, there is only so much amount of abstraction that a human brain can handle, and at times small details can change everything. As Alain Connes put it in the Princeton Companion, the most difficult step in a mathematical work is checking for mistakes.