> It is not wrong to treat algorithms as valid proofs.
I think that's what PP meant, i.e. if you want to differentiate between sorting algorithms in terms of efficiency, you somehow should encode this demand into the types (specification).
You can do that, yes. My argument is that you don't have to do that -- you can prove asymptotics or stability after the fact, having previously only given an algorithm as a proof of sortability.
Putting these properties in the specification assumes you already know (or suspect) that your algorithm has these properties; then you are simply verifying what you knew. If you develop your algorithm first, then want to analyze it in terms of (say) asymptotics, then not only is it far too late to change the type, you don't even know what the asymptotics are yet. You'd still like to treat the algorithm formally in order to determine those asymptotics, but since you don't know them yet, the algorithm can't inhabit a type that states those asymptotics outright.
I think that's what PP meant, i.e. if you want to differentiate between sorting algorithms in terms of efficiency, you somehow should encode this demand into the types (specification).