Yes.
I routinely write code in Haskell that I'm "not smart enough to write" by leaning on Curry-Howard very heavily. For me the Curry-Howard correspondence provides me with a lot of insight into how to better structure my code.
The view of types as propositions and programs as proofs matters more the more abstract you can make the propositions!
The more abstract you can make your propositions and hence more general your types, the more scenarios you'll be able to reuse them in. This reduces namespace pollution from a software engineering perspective and encourages code reuse for a deeply fundamental reason, not an ad hoc one.
Moreover, by making your types more general, you get fewer possible implementations that can type check. This gives you a lot of insight into why your code behaves the way it does and why it must behave that way.
For example it is actually pretty easy to muck up writing the state monad, but it is almost impossible to muck up writing the indexed state monad, despite the fact that the latter has a more complex type.
Improving the generality of your code via parametricity and Curry-Howard grants you stronger free theorems, which are laws you can use to reason about the behavior of your code just from the type signatures involved, without caring about the implementation of the function. This often allows you to achieve the OOP holy grail of encapsulation simply by following the same process that makes your types more general and your code more reusable, but in such a way that you aren't beholden to a programmer doing the right thing. You get the encapsulation in question "for free" from the types and the space of possible proofs.
If you go farther, and move up to the "Curry-Howard-Lambek" correspondence that gives you the 3-way bridge between types, propositions and category theory, you get to borrow even more tools across the divide. The insight into monads and comonads as a form of modality lets you reason about effect systems using modal possibility and necessity, the (!) modality in linear logic can be viewed as a comonad, linear logic can be viewed as the internal language of a symmetric monoidal category, etc.
This lets you move knowledge between pure mathematics, programming, even quantum physics -- after all, that is just another monoidal category. I routinely use trace diagrams from category theory when working with anything from database joins to knots to defining just the right monad to make my parsers work.
Once you know how that bridge works you can move a lot of information across it!