Nothing forces developers to write a complete specification of the algorithm. You want to have it both ways. If developers keep the spec concise but incomplete

Nothing forces developers to write a complete specification of the algorithm. You want to have it both ways. If developers keep the spec concise but incomplete, then you say the spec is incorrect so now you have to prove that the spec is correct. Ok, but people already use unit tests to sample the behaviour of a function so they already accept some degree of inaccuracy. By your logic you have to enumerate the entire input space otherwise unit testing is worthless. If developers decide to build a complete specification of the algorithm, you counter that the specification is now too long so they should not bother. You are basically arguing with yourself. The update argument doesn't make sense either, because you generally want to prove properties like absence of panics throughout your entire codebase. Again this is just a roundabout way of arguing against the very idea of a tradeoff.