If you are writing programs in Coq or another dependently typed programming language, these parallels between math and programming are not just incidental; they

If you are writing programs in Coq or another dependently typed programming language, these parallels between math and programming are not just incidental; they are one and the same. Theorems are stated as functions, whose type signatures reflect the theorem being proven. Even the gap that you mention at the end of your post is bridged, since the type checker will verify that your proof is correct (modulo the trust in the metatheory of the language itself, and its implementation). Things like refactoring, choosing more or less specific statements of theorems (e.g. more or less abstraction in a library), interfaces, etc, all become exactly analogous to the same kinds of problems faced in software engineering. It's really quite remarkable. (Disclaimer: I'm hardly an expert in these languages; I just dabble.)