Compare writing a proof in Coq to writing a normal program. That is far more equal in terms of what you're doing. Writing a proof for people implicitly assumes a mountain of background information and interpolation between statements that doesn't exist in programming.
