IMO, yes. Similar to the benefits of learning Haskel as a Javascript programmer, there are ideas better embodied in Coq that translate to all languages. For ex

IMO, yes. Similar to the benefits of learning Haskel as a Javascript programmer, there are ideas better embodied in Coq that translate to all languages. For example, the idea of strengthening & weakening the inputs/outputs of your lemmas, functions, or any abstraction is really central Coq. Constantly there is a tension between weakening your preconditions so your abstraction is easier to apply while also strengthening your postconditions so you get more leverage from you abstraction, or doing just the opposite so that implementing the abstraction is possible. After working with Coq almost exclusively for a year and then returning to regular programming, I find this is a concept I come back to constantly. It applies to any language. One example is creating library API preconditions & postconditions such that the API is useful to the caller but not so tight that there's no room to change implementation details as the maintainer. With API contracts in particular, it's usually possible to strengthen a postcondition and weaken a precondition without breaking compatibility so it's helpful to start with weaker postconditions and stronger preconditions to give you that flexibility. In regular languages, preconditions & postconditions is something that the language only helps you out partially. Even in Haskel this is true. Most of the contract is not enforced by the type system and can only be described in documentation. If your API takes in a "number", chances are there are bounds on what that number can be, e.g. non-negative or less than the length of the list. In Coq, all of this would be very explicit and machine enforced. When writing contracts now, I sometimes imagine what lemmas and witnesses I would have written or assumed in Coq and that helps me think about the trade offs. This concept often applies beyond APIs to the whole system architecture. What should that microservice require of its inputs and what guarantees can that storage system provide, etc.