3 ms·
"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
by RandomThoughts3 2y ago
"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 2y agoOh, 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.