If you aren't doing formal verification of programs, the other main use case of Coq would be using it to assist with coining a new domain-specific language, and

If you aren't doing formal verification of programs, the other main use case of Coq would be using it to assist with coining a new domain-specific language, and proving that the language meets certain requirements. If you have a concurrent program you can also try encoding a fragment with simplified semantics in Coq and prove the correctness of the program in Coq. https://softwarefoundations.cis.upenn.edu/current/plf-current/Smallstep.html https://softwarefoundations.cis.upenn.edu/current/plf-curren... Here is an example of that for a toy language.