Please correct me if I've misunderstood Curry–Howard, but the way I see it: In mathematics we can take a proposition, and then try to find a proof for it. Depending on the proposition, this can be extremely challenging. And in programming we can write the type of a function, and then try to write some implementation that our type checker will accept. If the function type is complicated enough, then finding _any_ program that has that type can be challenging. And Curry–Howard correspondence shows us that there's a deep connection between trying to find a proof for a proposition and trying to find any program that has a given type.

But when I program, then "trying to find any program that has a given type" rarely feels like the main problem I'm trying to solve. Depending on the program, I may want the program to do any of these things: run efficiently, conserve memory, have a good-looking and intuitive user interface, support multiple languages, be secure, be maintainable. If it's a web app, I want it to support multiple browsers. If it's a game, I want the challenge level to be just right. If it's a software instrument, I want it to sound good. You get the idea. So yes, there exists an isomorphism between programs and proofs, but I'm not really sure what to do with it, since the isomorphism doesn't preserve most of the properties I care about.

Dependently typed programming languages seem capable of defining types that express many aspects of a program’s specification.

Formal specification in that sense isn’t enough to guarantee that your game is challenging—but it’s an engineering discipline that helps make sure your implementation is correct, and that you have clear and well-defined intentions.

Curry-Howard and dependent types is far from the only way to use logic for reasoning about programs!

One cool thing I’ve seen is using linear logic to make prototypes of games. Linear logic is good for expressing rules that consume and produce resources, in a way that fits very well with many game rulesets. Thinking of games as logical systems means you can ask questions like “is level 3 possible to finish starting with the items found in level 2?” (A proof could be a sequence of actions that start with those items and eventually reach the level’s end state.)

Logical reasoning isn’t the only aspect of software development, just like structural engineering isn’t the only aspect of building houses.

What you're describing here (and this again is my interpretation) sounds more similar to 'Homotopy Type Theory'. https://en.wikipedia.org/wiki/Homotopy_type_theory

Homotopy Type theory also shows some deep connections between mathematics and programs, as the progress of the theory has bee characterised by building programmatic proofs _first_, to generate new mathematics. That's an inversion of the usual process.

Doing mathematics is really nothing like software programming. Yes, there is an isomorphism between proofs and programs, but that doesn't mean much for the vast world of mathematics outside logic

There are isomorphisms between any place of that vast world of mathematics and logic too.

Math is also constrained by fitness, not perfection. Just take a look on the number of unproved conjectures we keep around. It's just that the Math community generally places more value on proofs than the programming, but it is a continuous, and there are more tolerant subcomunities of mathematicians and very intolerant ones of programmers too.

I didn't mean that mathematicians don't write code; I meant that doing most mathematics isn't anything like doing programming, even when you're programming in Haskell. Just because two things are isomorphic doesn't mean they're used in the same way. For example, programming is formal but rarely rigorous; mathematics is the opposite.

Most mathematicians do work that is very different from most programmers. Some programmers do work that is similar to most mathematicians, and some mathematicians do work that is similar to most programmers.

Programming can be very rigorous, and mathematics can be very formal and not rigorous. There is a huge middle ground, sparsely populated between those.