Well, generally, first there has to be some things that you assume to be true - we'll call them axioms (somethings gotta be true, I mean can you prove that the natural number 0 equals the natural number 0). Then you come up with some properties about your algorithm that you want to ensure hold based on those axioms (or stuff already known to be true that are based on those axioms). So, for example, you may want to ensure that your algorithm does not change the length (or more generally the structure) of the input when sorting - e.g. if your sorted list came out with more elements than it went in with that wouldn't be sorting.

Now you don't need to have a formal proof for this right away (or at all if you don't want to really). A tool like "Quick Check" (Haskell, Erlang, ...) can help you do a quick informal check by making up a bunch of random list structures and running a unit test on all of them automatically. If your quick check property holds you may want to later try a proof and perhaps even see if something like ATS verification system is expressive enough to encode your proof or prove it for you auto style.

The benefit of the verification system is that it happens as static analysis (things that can be determined from reading the code rather than running it) the quick check stuff you need to run the code. A proof is a more complete check.

Please read the ATS (Coq, Agda, etc) stuff to learn from the experts.