Talk:Thierry Coquand

A fact from Thierry Coquand appeared on Wikipedia's Main Page in the Did you know column on 14 April 2023 (check views). The text of the entry was as follows:

Did you know... that Thierry Coquand won a SIGPLAN award for his eponymous proof assistant Coq, which was used to find a formal proof of the four color theorem?

A record of the entry may be seen at Wikipedia:Recent additions/2023/April. The nomination discussion and review may be seen at Template:Did you know nominations/Thierry Coquand.

Wikipedia

This article must adhere to the biographies of living persons (BLP) policy, even if it is not a biography, because it contains material about living persons. Contentious material about living persons that is unsourced or poorly sourced must be removed immediately from the article and its talk page, especially if potentially libellous. If such material is repeatedly inserted, or if you have other concerns, please report the issue to this noticeboard.

If you are a subject of this article, or acting on behalf of one, and you need help, please see this help page.

Biography

This article is within the scope of WikiProject Biography, a collaborative effort to create, develop and organize Wikipedia's articles about people. All interested editors are invited to join the project and contribute to the discussion. For instructions on how to use this banner, please refer to the documentation.BiographyWikipedia:WikiProject BiographyTemplate:WikiProject Biographybiography articles

Computing

	This article is within the scope of WikiProject Computing, a collaborative effort to improve the coverage of computers, computing, and information technology on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.ComputingWikipedia:WikiProject ComputingTemplate:WikiProject ComputingComputing articles
???	This article has not yet received a rating on the project's importance scale.

Did you know nomination

The following is an archived discussion of the DYK nomination of the article below. Please do not modify this page. Subsequent comments should be made on the appropriate discussion page (such as this nomination's talk page, the article's talk page or Wikipedia talk:Did you know), unless there is consensus to re-open the discussion at this page. No further edits should be made to this page.

The result was: promoted by Cielquiparle (talk) 07:44, 2 April 2023 (UTC)[reply]

(

Comment or view
Article history

)

... that Thierry Coquand won the 2013 ACM SIGPLAN Programming Languages Software Award for co-creating the Coq proof assistant? Source: https://awards.acm.org/award_winners/coquand_8654317
- Reviewed:

5x expanded by Partofthemachine (talk). Self-nominated at 17:25, 25 February 2023 (UTC). Post-promotion hook changes for this nom will be logged at Template talk:Did you know nominations/Thierry Coquand; consider watching this nomination, if it is successful, until the hook appears on the Main Page.[reply]

The hook as currently written is not intriguing to a non-specialist audience considering it assumes reader familiarity with all the terms and names mentioned in the hook. Otherwise the article meets DYK requirements and is free from close paraphrasing. The nominator has no prior DYK nominations so a QPQ is not required. Narutolovehinata5 (talk · contributions) 10:54, 27 February 2023 (UTC)[reply]

I agree, it's a bit confusing to read. How about something like:
ALT1: ... that Thierry Coquand was recognized by the Association for Computing Machinery for co-creating the eponymous Coq proof assistant? Wracking ^💬 21:21, 28 February 2023 (UTC)[reply]

While more understandable, I'm not really sure if it's still interesting to a non-specialist audience. Given that this is tech-related I'd like to hear DigitalIceAge's thoughts on ALT1. Narutolovehinata5 (talk · contributions) 01:10, 1 March 2023 (UTC)[reply]

Agree that the hooks require foreknowledge of SIGPLAN and its eminence to be interesting. Why not mention something about Coq itself? E.g.
ALT2: ... that Thierry Coquand's namesake Coq proof assistant was used to find a formal proof of the four color theorem? Or if we want to mention the award, we can say
ALT2b: ... that Thierry Coquand won a SIGPLAN award for his eponymous Coq proof assistant, which was used to find a formal proof of the four color theorem? A bit long but more interesting IMO. DigitalIceAge (talk) 01:39, 1 March 2023 (UTC)[reply]

I personally like ALT2b the best. Partofthemachine (talk) 22:09, 1 March 2023 (UTC)[reply]

I like both ALT2s better than the ALT1 I proposed. Is there a typo in it? ("formal proof of*...")? Only other concern is if there's an issue calling it "his" as he's among several creators. Wracking ^💬 22:54, 1 March 2023 (UTC)[reply]

I changed "proof or" to "proof of" in both places. MANdARAX • XAЯAbИAM 22:17, 9 March 2023 (UTC)[reply]

Still waiting for Partofthemachine to chime in on the new proposals before continuing the review. Narutolovehinata5 (talk · contributions) 02:41, 13 March 2023 (UTC)[reply]

I already did, I said I preferred ALT2b. Partofthemachine (talk) 21:58, 13 March 2023 (UTC)[reply]

I'm not sure how I missed that, my apologies. This is ready for a full review. Narutolovehinata5 (talk · contributions) 23:10, 13 March 2023 (UTC)[reply]

New enough, long enough. ALT2b short enough and sourced (as is every paragraph). No neutrality problems found, no copyright problems found, no maintenance templates found. QPQ unnecessary and image properly licensed. Good to go.--Laun chba ller 16:07, 27 March 2023 (UTC)[reply]