So long as the list is finite and no being modified outside of sort that can be done for some sort algorithms. Bogo sort wouldn't. If < works as expected (a<b means b<a) most algorithms will sort algorithms terminate, and a few don't even need that (though < working is needed to prove the result is ordered ).

Gödell showed there are algorithms that we cannot prove, but he did that with self referencing algorithms which we rarely use.

Of course the most commonly used CS algorithm is proved correct in various properties, that wasn’t my point.

Still, you can’t even in theory prove every interesting property about any problem/algorithm.

Sure, but i'm contending those algorithms we cannot prove are mostly not used in programming in the real world.