The two are different things, and in fact much more different in practice than they would be in theory.
A formal correctness proof proves something about the behaviour of an algorithm. For instance, it might investigate the invariants applying to the data as it is transformed by a sorting algorithm, and prove that if the algorithm terminates, every element is larger than the previous one. This kind of proof can be rigorous, i.e. if it's done correctly the algorithm cannot be wrong in this respect.
In practice, algorithms must be embodied in computer code, and it's usually infeasible to prove that a given bit of code accurately represents the algorithm that you want. (That would require formally proving the behaviour of the compiler, the standard library, the virtual machine, etc.) It gets a little easier the more similar the programing language is to the mathematical notation you've used in the formal proof, but not much. (The code running in central systems of the Space Shuttle was said to be almost a perfect mathematical notation itself, but not very pleasant to program in.)
It's much more cost-effective to actually run the code on judiciously chosen inputs and verify that it produces the expected outputs. This has the disadvantage that you can never be certain that there isn't an error in it - it might behave for those input/output pairs you haven't tested (and there are usually more pairs than you can test, or you wouldn't need a computer program to do the work in the first place), or worse, the code might be subtly non-deterministic or context-dependent in way that your tests don't expose.
But in practice, most errors that affect a computation can be exposed with intelligent checks, and if you keep a record of known errors and test cases verifying they cannot recur, the quality of code can generally be made good enough to be of business value. Certainly it's a better idea to run unit tests, integration tests and user acceptance tests and get something out the door that people will pay for than to conduct a lengthy, expensive formal proof that overlooks a subtle deviation between the written specification and the actual expectations of the customer. So in the real world, the two are almost completely distinct activities.