Please do not reply directly to this email. All additional comments should be made in the comments box of this bug report. Summary: Review Request: coq - Coq proof management system https://bugzilla.redhat.com/show_bug.cgi?id=450323 dwheeler@xxxxxxxxxxxx changed: What |Removed |Added ---------------------------------------------------------------------------- CC| |dwheeler@xxxxxxxxxxxx ------- Additional Comments From dwheeler@xxxxxxxxxxxx 2008-06-06 14:28 EST ------- This is excellent - I'm glad to see this package!!! I have a nit about this description, I think it needs to be clearer. I realize it's similar to the Debian text, but I think the Debian text isn't clear at all. Also, Coq is an _interactive_ prover, not an automatic prover, and I think it's important to note that. How about this description instead (starting with the text on their website, but changing "done with" to "interactively developed using", and adding in the stuff from the submitted description): *** Coq is a formal proof management system: a proof interactively developed using Coq is mechanically checked by the machine. In particular, Coq allows users to define functions or predicates, to state mathematical theorems and software specifications, to develop interactively formal proofs of these theorems, and to check these proofs by a relatively small certification "kernel". Sets of definitions and theorems can be saved as compiled modules and loaded into the system. Coq has been used to formally prove claims about real programs (see the Coq website for more). Coq uses first order logic, and is implemented with OCaml. *** Thanks!! -- Configure bugmail: https://bugzilla.redhat.com/userprefs.cgi?tab=email ------- You are receiving this mail because: ------- You are on the CC list for the bug, or are watching someone who is. _______________________________________________ Fedora-package-review mailing list Fedora-package-review@xxxxxxxxxx http://www.redhat.com/mailman/listinfo/fedora-package-review