This may be off topic, but I really appreciate experts here kindly answering my elementary questions.
Zulip Coq seems to be friendly to beginners. (^o^)
yes I think the Proof Assistant Stack Exchange will not be friendly for elementary questions by design, e.g., the question will be marked quickly as a duplicate and closed without followup...
Indeed, so it's important to keep the friendly welcoming environment here on Zulip. I guess the community page on the website will need to be adapted to explain the distinction.
normally there is a wide gulf between "free-for-all tech support" (Zulip) and "curated Q&A" (StackExchange). Although I see that people sometimes use SE for the former. But we can't really curate all that well on Zulip.
Also, I think we can be clearer that the "Coq users" stream (including maybe math-comp users) is the true home of tech support. Other streams typically have different purposes, such as coordination and debate, in my view at least.
It seems to me that streams like Equations devs & users, Ltac2, MetaCoq, Proof General users, VsCoq devs & users are also for tech support.
partly, sure. But I don't think we can or should mandate/recommend the same experience there as in Coq users (1k people subscribed, default stream)
New stackexchange sites are not like stackoverflow. I agree that on stackoverflow it can be very harsh to users, but the newer stackexchange sites in my experience have been welcoming. I don't expect any questions to be closed as duplicates this early on since there are hardly any questions yet.
CS Theory Stack Exchange is really bad in my opinion, I saw multiple closings of issues due the closer saying that "interactive proof" only has to do with PCP theorem and the like, and they can't accept it having another meaning
I really think any effort that includes both CS Theory A and B is dead at the outset.
My lab has both theory A and B and people manage to talk to each other (even though they sometimes realize that they speak different languages) :laughing:
well, communicating and collaborating are different.
Anyway, I think that the new site being more limited in scope, it will be easier to provide a welcoming atmosphere (even if that means redirecting some newcomers to Zulip for tech support that doesn't fit the SE model).
Théo's counterexample is interesting but might not invalidate the rule... luckily this SE is Theory-B only.
@Karl Palmskog I'd vote to reopen, and have some reputation on TCS.
I haven't been there in a while, but I don't think that problem is insurmountable.
well, this was a while ago, and to be honest it only takes a few instances of this happening for me to lose interest. I imagine it's similar for other theory B people.
I guess I'm also affected by working close to some people who were reputation mining questions on regular StackOverflow. It was depressing to watch and hear about, e.g., it was obvious that thoughtful extensive answers would always come last. And people who didn't write such answers were the ones moderating everything.
Last updated: Jun 01 2023 at 12:01 UTC