A proposal by Andrej Bauer: http://math.andrej.com/2021/11/20/proof-assistants-stackexchange-site. I hope this is not duplicate here
The proposal successfully reached the commitment stage, let's help the proposal reach the beta stage!
The proposal has completed the commitment stage. This means that the site will go into private beta soon. People can still commit to be invited to the private beta.
During the private beta, it would make sense to try to migrate some Frequently Asked Questions, both from https://github.com/coq/coq/wiki/The-Coq-FAQ and that people have encountered here in Zulip or in Discourse / Coq-Club. As I wrote in a much upvoted comment in a previous discussion, people can self-answer their questions on Stack Exchange, so this means that Zulip users answering questions and noticing that some of them are frequently asked can create a corresponding (canonical) question / answer on Stack Exchange.
since Stack Exchange considers new users pariah, I would recommend that people with a lot of SE reputation to do all this work (otherwise I think it will get stuck in the various pariah filters they have)
Stack Overflow works like you say and is pretty unwelcoming. But the good thing of this being a new site is that it will have much fewer barriers of entry and basically everyone will start on equal footing (long time SO users will have to rebuild their "reputation" on this new site).
but it looked to me like reputation from other SE carries over? Otherwise, why does it rank commits by reputation?
Usually when you join a new SE site, you only get a boost of 100 points for being reputable on other sites.
Indeed, @Théo Winterhalter is correct. I should have put "virtually" in front of "equal footing" for this reason.
sigh, it seems people with no rep don't even show up in the committed list... Apparently some artifact due to account email verification.
"Academic or Research-Level Student" seems a bit over-used, as was already pointed out by Andrej: https://twitter.com/andrejbauer/status/1462337362843914240
Ha ha, @pigworker marked himself as "Academic or Research-Level Student". What potions has he been drinking? And I bet he's lurking somewhere around here.
- Andrej Bauer (@andrejbauer)I think that many of us interpreted this as "Academic OR (Research-Level Student)" and not as "(Academic or Research-Level) Student". English. Sigh!
yes, I also think that's how some non-native speakers may have read it. And then others will interpret it as false modesty... sigh indeed
But isn't Conor McBride (a.k.a. "pig worker") a native English speaker? Do you think that it's really false modesty on his part or is it proof that this phrase has several interpretations, including for native English speakers?
he is a native speaker and he was likely trolling a bit as Andrej says. So probably no misunderstanding on his part. He may even have been prompted to select it due to the ambiguity.
On the other hand I was afraid of appearing as pompous for selecting expert because I understood the item as "student".
anyway, I'm looking forward to the fair and balanced answers on subject reduction and the like...
As I wrote in my note, the main advantage of SE questions is their insanely high ranking in search engines. I don't really get how it can be a place where people actually hang around (other than for winning the reputation rat race)
I mean, if I'm not the person who asked the questions, then SE questions is the only place I know where I can easily go and check out the answer that worked. If I wanted to race for reputation, I probably wouldn't hang on the Coq SE though. :)
the point is that (in my opinion), nobody should "go and check" SE. You should use your favorite search engine, find the SE answer, read it, then get out...
I wouldn't be surprised if the company behind SE has some special deal with Google et al.
I check it to answer questions.
but why do that, if you're not into the reputation stuff?
To help others?
What is wrong with willing to help?
I think Théo Zimmermann suggested the best approach: instead of waiting for people to ask SE questions, pre-ask and pre-answer (since we already know most of the time what questions are and will be)
I don't mind people helping, but I don't think SE is the best way to do that
Karl Palmskog said:
I don't mind people helping, but I don't think SE is the best way to do that
It depends on whom you want to help and in what context. The principle of SE is that questions (not just answers) should be of high quality. Unfortunately, the reputation game isn't working so well since people will rush to answer basic questions to get the most rep points. But I think that in the context of a smaller community, it can work better than it does on SO.
Karl Palmskog said:
I don't mind people helping, but I don't think SE is the best way to do that
What do you think the best way to help?
BTW, we already have an active SE integration here in the Coq Zulip for every question tagged Coq. I expect it should work fine for the new site once we are out of private beta.
as I implied above, I think the best way to help is to curate good questions / answers via other forums, then self-ask, self-answer on SE to get their insane search engine priority
I agree, though this is not conflicting with answering good questions with good answers when they happen to be posted.
And with the Zulip integration, following the questions being asked shouldn't be too difficult.
I see your point of view, but I still worry about flood of basic repeated questions (crowd detection of duplicates is hard) and reputation mining
Ah OK, this is where our expectations for the future of this site differ. I expect a bump in the number of questions per day, but probably not to the point that it will become a flood. But if it does, then this will need another management strategy.
Anyway, the site will be what we do of it. If we see people asking very basic and repeated questions, we can decide to redirect them to Zulip chats for more interactive help sessions, while focusing on answering the good questions that will help a lot of people in the future.
I also hope that longer answers will be tolerated, I've seen quite lot of shooting down exposition on SE (in fact this is encouraged by winner-takes-all reputation points)
My experience is with answering questions on low-activity sites or tags and in this case, there is not such a rush to be the first to answer, so long answers are well-received and encouraged. In fact, even if you post an answer after one has been marked as accepted, the asker can still change the accepted answer, or the new answer can still receive many upvotes.
just to clarify if someone still wonders, I meant
why do that
in the sense of
why pick that particular option/method of helping people, among all the ones available
which I think should be reasonable to ask, even if we assume "helping is good" in general
hmm, when the PA SE goes into beta, we may even consider having a Zulip stream dedicated to it, or what do you think @Théo Zimmermann? Could be a good way of coordinating good answers (and questions).
I'm optimistic about this experiment. Stack Overflow's impact & utility for working engineers cannot be denied. (Other platforms surely exist; I'd be excited to see proposals for their use as well.)
The creation of a new subsite will create new ways for people to participate in the community. IMHO the "worst case" is that the subsite winds up consisting of the same people who are already on all of the mailing lists and Zulip chats. Or another "worst case:" the site never gets enough traffic to move out of Beta, or is eventually deleted due to inactivity. To me, the real measure of success will be whether or not it grows & scales.
Karl Palmskog said:
hmm, when the PA SE goes into beta, we may even consider having a stream dedicated to it, or what do you think Théo Zimmermann? Could be a good way of coordinating good answers (and questions).
That's a terrific idea (if enough people are willing to participate in this coordination effort). Please upvote Karl's post if you'd be interested in joining such a stream.
the main reason to coordinate I see is that we don't want duplicate effort, e.g., both Théo Z. and I working to answer some Coq proof engineering question in parallel
It would be great if there was enough sustained interest that duplicate effort winds up being a problem :sweat_smile: I like your proposal because I'm worried that questions will go unanswered after the initial excitement wears off! (Upvoted)
@Tim Carstens Look at this: https://stackexchange.com/filters/299857/questions-tagged-coq-on-stackexchange-sites. Questions about Coq on SE sites already get answered as of today. I don't expect this will change, except if we get too many questions for what experts are ready to answer.
I also saw that to get out of beta, there has to be sustained activity, they even give beta stacks a "grade" in each activity measure: https://area51.stackexchange.com/proposals/125174/cardano
5.9 questions per day: Okay – 10 questions per day on average is a healthy beta, 5 questions or fewer per day needs some work. A healthy site generates lots of good content to make sure users keep coming back.
These measures are outdated according to a response on the Proof Assistants proposal. Let me find the link.
The "pre-ask question" model only works for question of a rather general scope. There are techniques that really only make sense in the context of concrete examples, which are best illustrated when askers provide the examples that are relevant to them, when they don't have the expertise or the time to read CPDT and figure out what is relevant and how to apply it.
@Théo Zimmermann Excellent point :+1:
@Li-yao but we do have many examples across Coq-Club, Disourse, Zulip, etc. I agree about using examples, but I think there are low-level specific questions that are common also.
Do you think that simply answering people's question is counter-productive? I think that even ill-asked questions are of value, because they might reflect how others might think of a problem the way experts don't.
When on the side of finding a solution to my problem, sometimes, finding someone else's struggle helped understanding what my own problem was.
I think it's obvious that many questions (on SE and elsewhere) are very poorly formulated, such that they are nearly unsalvageable. In particular, it's often clear the user has made little effort to produce a small example that reproduces or illustrates their problem. We are as a community mainly interested in the collection of quality questions & answers, not that each user gets their personal question answered.
People who answer questions have limited time which means there can be a substantial opportunity cost to answer bad questions for the community.
Even with a database of quality Q&A I wouldn't know how to search it without already knowing the answer.
search engines are pretty good at setting that up (i.e., good at searching SE), and I think there are probably code-based interfaces to the SE API based on learning and so on. Could be worth looking into, but I still think the quality Q&A is the main thing.
While I think that technically SX has managed to be very useful for a lot of technical questions (BTW, I access it via DuckDuckGo and they seem to have just as much of a deal with them as with Google ;-), I'm worried about the fact that those questions&answers are locked in some company's servers. That's why I largely stopped contributing to it. If only we could archive the data elsewhere.
they have an interface/API to retrieve both questions and answers, and the license is CC-BY-something. In my opinion a "Coq Stack Exchange Working Group" could make sure all Coq questions and answers are regularly backed up (but preferably only the quality ones).
Indeed, CC BY-SA version 2.5, 3.0 or 4.0 depending on the date of the latest revision (and the UI and the API provide this information) as was explained in a post you shared earlier in a previous discussion (https://meta.stackexchange.com/questions/347758/creative-commons-licensing-ui-and-data-updates/).
they have an interface/API to retrieve both questions and answers
So I heard but I still haven't seen a tool that performs actual usable backups (e.g. that can produce some kind of read-only barebones mirror). I haven't actively looked for it, admittedly.
@Stefan Monnier Not exactly what you're asking, but such "backups" are clearly done in practice (at least for StackOverflow). That's visible when googling a question and seeing Google find an SO clone.
(which, BTW, seems unlikely to ever happen if SX had a special deal!)
there are multiple servers with snapshots of SO questions, thanks to the CC-BY license.
those are presumably made by less reputable companies, but it seems to confirm backups are essentially possible.
A StackExchange chat room for the ProofAssistants proposal has been setup: https://chat.stackexchange.com/rooms/131732/proofassistants-temp
The most useful info I could get so far from this chat room is an estimation that the private beta could start on the 7th or the 14th of December and the public beta should happen 3 weeks later, but probably after Christmas.
Proof Assistants private beta launch will take place in January 2022
Since we want all proposals to have the best chances of thriving as possible, the Community Team has decided to postpone this proposal's launch into private beta to January 2022, in an attempt to minimize the impact of the upcoming end-of-year holidays in the site's chances of success.
Additionally, the proposal sped through its definition and commitment phases, which we believe hasn't allowed for some discussions that usually take place during those phases — such as deciding on a name and URL for the site — to come to a consensus. As such, we invite those of you who've committed to this proposal to try to have those conversations between now and the first couple of weeks of January 2022. At that time the Community Team will help y'all tie whatever loose ends need to be tied, and prepare the site for launch into private beta.
No better way to kill momentum, but go figure...
Last updated: Jun 01 2023 at 12:01 UTC