[RandomThoughts3]

"The C standard formalised in Coq" is literally the title of Robbert Krebbers's PhD, that gives you an idea of how usual and easy it was.

The fact that you can formalise a specification in order to prove it doesn't make Coq a specification tool.

[auggierose]

Oh, if you define specification as something that should be done by people without a PhD, you might have a point.

I don't think software that needs specs should be done by people without a PhD. Jokes aside, I am not saying that Coq is an easy or simple specification tool. But of course it is a specification tool. Actually, it is one of the very few serious specification tools out there.