It is, and Coq is a piece of software to prove theorems. The context in which it is used makes it trivially inoffensive.

Personally, I spent a semester trying Coq and I couldn't get used to it. My professor loved Coq, though. He was a mathematician, so it wasn't a huge surprise.