It's hard to say exactly. It will teach you to think of programming in an entirely new way.
Will that make it easier to write good code elsewhere? Almost certainly if you're not familiar with mathematical proof (maybe you took a discrete math course before). If you know what it is to prove then you'll learn an interesting deep connection between programming and proving.
You probably don't want to prove things in your programs. Not really. Even after you learn Coq it's too difficult to do day-to-day.
But proofs do not work without being completely consistent in the same way that good programs are. So you can learn a lot of techniques for good programs from techniques for good proofs. Coq rejects bad proofs, so it can be good practice.
Finally, Coq is unashamedly higher-order. The chops you gain working with it will translate more or less directly to better functional programming comprehension.
Will that make it easier to write good code elsewhere? Almost certainly if you're not familiar with mathematical proof (maybe you took a discrete math course before). If you know what it is to prove then you'll learn an interesting deep connection between programming and proving.
You probably don't want to prove things in your programs. Not really. Even after you learn Coq it's too difficult to do day-to-day.
But proofs do not work without being completely consistent in the same way that good programs are. So you can learn a lot of techniques for good programs from techniques for good proofs. Coq rejects bad proofs, so it can be good practice.
Finally, Coq is unashamedly higher-order. The chops you gain working with it will translate more or less directly to better functional programming comprehension.