This really depends on what you're doing. I suppose most of the code I've written in the last two decades wouldn't have profited from using coq. BUT then there'

This really depends on what you're doing. I suppose most of the code I've written in the last two decades wouldn't have profited from using coq. BUT then there's CompCert, an optimizing compiler written in coq [I'm affiliated, but not working on it directly]. If you're building safety critical stuff (like in failure == people die) something like this might be interesting. Of course, for a C compiler the requirements are less prone to change than e.g. some SAP-style business application. As a dev, coq is just another tool in your belt and being a good dev means knowing when to use what tool.