(https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...)
You only get glimpses of that correspondence with procedural programming. It's much more apparent with functional programs though.
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.
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.
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.
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.
Programming can be very rigorous, and mathematics can be very formal and not rigorous. There is a huge middle ground, sparsely populated between those.