The trivial sorting spec is actually very useful, it's just not complete. While knowing that your sorting program meets the complete spec proves it works correctly, if you wrote it intending to be a sort algorithm, and you have proven it meets the trivial spec, and you have a few unit tests, that's still very good-but-not-foolproof evidence it's correct.

do you have a reference to anywhere that discusses this further? It seems pretty trivial to me