> If we take 'specifications' one level further and actually want our algorithms to be proven correct, as in, by a proof assistant it is quite unclear that this possible or desirable.
It is not only possible, it is how dependently-typed languages/proof-checkers like Agda work.