Talk:Coq (software)

Relevancy of the described proof and Benjamin Werner

Why was the 4-color proof chosen? Especially as it is taking more space than the description itself.

Is it really justifiable that Benjamin Werner is mentioned in the description? Thierry Coquand should definitely be mentioned as Coq is built around his research but what has Benjamin Werner done that he's more important than all the other people that worked on Coq? —Preceding unsigned comment added by Mikolasj (talk • contribs) 18:03, 27 April 2009 (UTC)

Confusing

This article has several definitions, whch are confusing on their own, and are not seperated. Fatalserpent 04:23, 21 May 2006 (UTC)

Diagrams/Examples

Would it be worthwhile to add some example Coq scripts, with proofs and brief explantions. Possibly to show what can be proved (including principles of classical logic as opposed to modern prop too?), and various constructs within Coq such as inductive/fixpoint definitions (Peano numbers and trees strike me as suitable candidates)? I'm aware that this article shouldn't read like a Coq tutorial, but it may help to show the readers what Coq looks like, and what it's capable of. Pyrre (talk) 03:40, 23 December 2007 (UTC)

Pyrre, I'm sorry your request hasn't received a response in over two years. Sometimes that happens. Having been exposed to program proving (David Gries, The Science of Programming) in graduate school, I, too. would like to see some simple as well as real-life examples proven false or correct by this program, including actual output. I'm particularly interested in how it handles loops (see the Halting problem). If someone out there is familiar with this program, please expand the article. David Spector (talk) 19:28, 24 June 2010 (UTC)

Reflection not defined, very ambiguous.

The term 'reflection' is not defined here.

There are many types of 'reflection', but I guess that the reflection here means the same one as on the bottom of page:

Ω-consistent_theory

The hyper-link there refers to the wrong page and there should be a page for reflection as meant here (that page does not exist yet).

Lkruijsw (talk) 23:56, 20 December 2009 (UTC)

"Reflection" in the name ssreflect refers to https://link.springer.com/chapter/10.1007/978-3-662-07964-5_16 — a probably more accessible explanation is in http://adam.chlipala.net/cpdt/html/Reflection.html. But I don't think ssreflect belongs to this page anyway, and it only happens to be here because of the relation with the proof of the 4 color theorem. --Blaisorblade (talk) 10:26, 15 July 2018 (UTC)

Some needed facts

What language is Coq programmed in? Is there a scripting language?

For which operating systems are binaries readily available?

Solo Owl 18:57, 20 July 2013 (UTC) — Preceding unsigned comment added by Eall Ân Ûle (talk • contribs)

External links modified

Hello fellow Wikipedians,

I have just modified 3 external links on Coq. Please take a moment to review my edit. If you have any questions, or need the bot to ignore the links, or the page altogether, please visit this simple FaQ for additional information. I made the following changes:

• Corrected formatting/usage for http://www.inria.fr/rapportsactivite/RA2004/logical2004/uid40.html
• Corrected formatting/usage for http://www.msr-inria.fr/news/feit-thomson-proved-in-coq/
• Added archive https://archive.is/20130415082551/http://math-classes.org/ to http://math-classes.org/

When you have finished reviewing my changes, you may follow the instructions on the template below to fix any issues with the URLs.

This message was posted before February 2018. After February 2018, "External links modified" talk page sections are no longer generated or monitored by InternetArchiveBot. No special action is required regarding these talk page notices, other than regular verification using the archive tool instructions below. Editors have permission to delete these "External links modified" talk page sections if they want to de-clutter talk pages, but see the RfC before doing mass systematic removals. This message is updated dynamically through the template {{source check}} (last update: 18 January 2022).

• If you have discovered URLs which were erroneously considered dead by the bot, you can report them with this tool.
• If you found an error with any archives or the URLs themselves, you can fix them with this tool.

Cheers.—InternetArchiveBot (Report bug) 01:20, 13 August 2017 (UTC)

what does this means ?

"CompCert: an optimizing compiler for almost all of the C programming language which is fully programmed and proved in Coq."

I understand the "programmed" part of the sentence, not the "proved": what's a "proved" compiler? — Preceding unsigned comment added by 185.24.185.192 (talk) 11:57, 17 August 2018 (UTC)

Would be nice to give more credit to Coq adding something like this: ` In the formalization system for univalent foundations that is based on Martin-Löf type theory and its descendants such as Calculus of Inductive Constructions, the higher dimensional analogs of sets are represented by types. The collection of types is stratified by the concept of h-level (or homotopy level). ` — Preceding unsigned comment added by 50.35.98.163 (talk) 20:38, 20 May 2020 (UTC)

Requested move 5 November 2023

The following is a closed discussion of a requested move. Please do not modify it. Subsequent comments should be made in a new section on the talk page. Editors desiring to contest the closing decision should consider a move review after discussing it on the closer's talk page. No further edits should be made to this discussion.

The result of the move request was: moved. (closed by non-admin page mover) Elli (talk | contribs) 19:49, 12 November 2023 (UTC)

---

Coq → Coq (software) – Not a primary topic. Either Coq or COQ should be a disambiguation page, and redirect Coq (disambiguation) and COQ (disambiguation) to its disambiguation. Coq may also refer to Coenzyme Q, Coquihalla, and Cock. 176.33.244.42 (talk) 19:20, 5 November 2023 (UTC)

If Coq is moved to Coq (software), then move COQ (disambiguation) to Coq and redirect Coq (disambiguation) there. 176.33.244.42 (talk) 01:39, 6 November 2023 (UTC)

Support There is no clear primary topic between Coenzyme Q and this software; the others mentioned by nom are a WP:PTM and an implausible misspelling. I also found attestation to the use of the acronym COQ for cost of quality. –LaundryPizza03 (dc̄) 16:48, 12 November 2023 (UTC)

The discussion above is closed. Please do not modify it. Subsequent comments should be made on the appropriate discussion page. No further edits should be made to this discussion.