3 ms·
Of course Coq is also a specification tool. C compilers have been formally verified with Coq. So you have a spec for C in Coq.
by auggierose 2y ago
Of course Coq is also a specification tool. C compilers have been formally verified with Coq. So you have a spec for C in Coq.
- 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.