Hacker News new | ask | show | jobs
by RandomThoughts3 655 days ago
No, it’s not. Gallina is not a specification tool in the way TLA+ is (even if coq calls it its specification language). Gallina is a language used to write mathematical statements which you intend to prove. It’s not designed to write specifications.

Coq is definitely not a specification tool. You can probably prove a specification with it in the same way you actually can do symbolic manipulation with C if you really want to. It still remains an interactive prover.
1 comments
auggierose 654 days 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.
link
RandomThoughts3 654 days 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.

link
auggierose 654 days ago
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.

link