The algorithms for the problem I am working on become more and more complex as I try to improve their performance. They already span several pages with cases and sub-cases, and will probably become even longer. I am worried that there might be mistakes that are difficult to notice.
As a programmer, I am used to writing detailed test-cases to test my programs, but the algorithm is written in pseudo-code (it is not easy to implement). What ways can you recommend for testing the algorithm?
This is an excellent question: how do we know that a complex piece of mathematics is correct? The (by now) traditional point of view is that if we succeed in proving something then it must be correct. Unfortunately, this point of view is a tad naive. Indeed, published papers often contain wrong results, and these can remain unnoticed for decades. Some high-brow examples can be found in Voevodsky's talk, and this is a notorious issue especially in cryptography and distributed computing, two fields with extremely complicated definitions and proofs.
The most stunning example, however, must be the gap in the proof of the classification of finite simple groups: the result was announced in 1983, but only in 2004 did Aschbacher and Smith publish two monographs (!) covering one of the cases. In 2008 a further gap was filled by Harada and Solomon who found, quoting Wikipedia, "a case that was accidentally omitted". Should we believe the proof now, then?
Another problem which has seen its share of wrong proofs is the four color theorem. The first two proofs, dating to 1879 (Kempe) and 1880 (Tait), were found wrong in 1890 and 1891, respectively. In 1977 Appel and Haken announced a solution, containing a very length case analysis. It was not surprising, then, that a small error was found around 1986. While the error was corrected, doubts remained. The matter was finally put to rest in in the computerized formal proof by Gonthier et al. (2005), formalizing the earlier "second generation" proof of Robertson, Sanders, Seymour and Thomas from 1996.
What is a computerized formal proof? The idea is that if you had a completely formal proof of each and every statement, then as long as we trust our proof system, then we can be sure that the result is correct. (Unfortunately, as Gödel showed there is no hope in showing that the proof system is consistent, so this is an article of faith.) As Russell and Whitehead exemplified in their Principia Mathematica, writing formal proofs is difficult. Instead, the idea is to use a proof assistant which gets hints and converts them, somehow, to a formal proof which can then be independently checked. There are several of these proof systems around, but the most popular nowadays seems to be Coq.
What if the reviewers don't believe your proof? This is the situation that Thomas Hales found himself in after proving (or so he claims) the Kepler conjecture on sphere packing. The reviewers gave up after spending a year of reviewing, saying that while they were unable to find any mistake, they are not completely certain that the proof is correct. In response, Hales decided to formalize his proof, starting up the Flyspeck project, now in its eleventh year. In a few more years the proof would probably be complete. Clearly this amount of effort is unreasonable for the everyday mathematician.
Can proof assistants be improved? Voevodsky has been developing Homotopy Type Theory, a Coq overlay for algebraic geometry, and claims that he is using it daily to verify his proofs. Last year Gonthier et al. formalized the proof of the Feit–Thompson theorem in group theory in Coq, thus laying the ground for formalized group theory results. Yet even these projects are missing a lot of background which will be needed to formalize research in theoretical computer science. Even after such a framework has been developed, it will still be rather time-consuming to turn the commonplace sloppy TCS proofs into formal attire.
So what are you to do? In your particular case, you are designing an algorithm, so you have the distinct advantage of being able to test your algorithm. (The Curry–Howard correspondence shows that every proof corresponds to an algorithm, but in your case the relation is clearer.) Perhaps there is a trivial algorithm which is very slow, and you could compare it to your algorithm. Or perhaps it is an NP-type problem, in which the solution is easy to verify but hard to find.
Do people actually verify their algorithms usually? I doubt it, unless they are in a field such as computational geometry in which their algorithms are actually being used. What people usually do is do their best to check their proofs, crossing all ts and dotting all is. That means avoiding phrases such as it is easy to see that. Having done that, they kindly ask a few other people to read through their proofs. Then they submit the paper to a journal, and if they're lucky then the referees will do another pass.
Even after all this, mistakes are occasionally found, but this is just part of life. Usually, these mistakes can be corrected easily, demonstrating that our formal sense of certainty is limited: true mathematics "works" even if not completely valid formally, as has been argued by a few philosophers, most of them coming from the ranks of practicing mathematicians. Wrong algorithms point the way to correct algorithms, as they bring new ideas. So don't worry too much, just do your best.
If you are working on "improving performance" of pseudocode, I'd tell you to forget about that. War stories of people optimizing the wrong part of a program are a dime a dozen. Perhaps the most hilarious one involved an early FORTRAN compiler for Unix. The programmer noticed a function he estimated would be called each 10 or so compilations, and took a week making it faster. The result was fast enough, and was shipped. This was still AT&T internal, so each time the compiler crashed the programmer got an email with the details. Some two years later, and a few million compilations, the compiler crashed in the "optimized" function. It turned out it would crash each time it was called. Measure before going on "improving performance". Programmers are normally wide off the mark on where the resources are spent. And it just might be that the straightforward code is performant enough, better spend your time at the beach (or wherever else you like). Performance improvements make the code harder to understand (and convince yourself/others it is correct!) and maintain, most "simpler" rewriting to get better code is done automatically by the compiler nowadays; and except for extreme cases your time is much more valuable than the computer's.
