I had experience both of writing programs and writing proofs including proofs in formally verified languages, e.g. Coq, Agda. First of all, I think that the au

I had experience both of writing programs and writing proofs including proofs in formally verified languages, e.g. Coq, Agda. First of all, I think that the author underestimates the complexity of writing correct programs. What if integer overflow occurs? What is some exceptions happens somewhere? Programmers rarely consider all the pathological cases, while mathematicians must consider all of them. If program works most of the time, it's good enough for programmer but not good enough for mathematician. Second, thanks to Curry Howard Correspondence, every formal proof has a corresponding program which 'constructs' a result of the theorem from preconditions, so, the proof is basically a program (and vice versa in a typed programming language).