Comment by inigyou

Note this doesn't make it useless, just not watertight. Proving that the output of a sort algorithm is a sorted list is genuinely useful and catches a lot of potential bugs. If your sort algorithm is "return []" you'll certainly notice that while writing the proof and fix it. It'll also be caught easily by any unit test.

It wouldn't catch all bugs - merge sort recursing on the same half of the list both times would return one item N times, which is sorted, and is a plausible enough mistake to make.