That is an opinion that many do not share. FWIW, I framed my response as an opinion; you gave yours as a blanket statement. It is not wrong to treat algorithms as valid proofs.
In a dependent type theory, propositions are represented as types; the proposition that "all lists can be sorted" could be represented represented as the type "forall (t : Type) -> (le : Ordered t) -> forall (xs : List t) -> exists (ys : List t). (Increasing le ys, PermutationOf xs ys)". A proof of this proposition is exactly a program (algorithm) with that type; the sorted list is the `ys` component of the returned existential product. Yet the inhabitants of this type are not graded by asymptotics or stability; any sorting algorithm will do.
In a setting where inhabitants of the above type are distinguishable, you could then write proofs of asymptotics or stability against individual algorithms. That is, the proofs of the sorting proposition are themselves the subjects of subsequent propositions and proofs thereof.