[Bug 450323] Review Request: coq - Coq proof management system

[bugzilla at redhat.com]

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 at dwheeler.com changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |dwheeler at dwheeler.com




------- Additional Comments From dwheeler at dwheeler.com  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.