Curry-Howard isomorphism does not mean the same practices that are performed in mathematics research must be applied to writing software.

Some aspects of language design are reinventing wheels invented by the math community. This is far from constituting the set of "writing software" or "software engineering".