Template:Did you know nominations/Thierry Coquand

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)

Thierry Coquand

(

)

... 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.

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)

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)

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)

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)

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

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)

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

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

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

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)

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)