Yosuke Ito (Nov 24 2021 at 10:21): Yosuke Ito (Nov 24 2021 at 10:21):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^)
Karl Palmskog (Nov 24 2021 at 10:45):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...
Théo Zimmermann (Nov 24 2021 at 11:03):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.
Karl Palmskog (Nov 24 2021 at 11:20):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.
Théo Zimmermann (Nov 24 2021 at 11:34):It seems to me that streams like Equations devs & users, Ltac2, MetaCoq, Proof General users, VsCoq devs & users are also for tech support.
Karl Palmskog (Nov 24 2021 at 11:35):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)
Ali Caglayan (Nov 25 2021 at 16:51):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.
Karl Palmskog (Nov 25 2021 at 16:53):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
Karl Palmskog (Nov 25 2021 at 16:54):I really think any effort that includes both CS Theory A and B is dead at the outset.
Théo Zimmermann (Nov 25 2021 at 17:00):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:
Karl Palmskog (Nov 25 2021 at 17:00):well, communicating and collaborating are different.
Théo Zimmermann (Nov 25 2021 at 17:01):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).
Paolo Giarrusso (Nov 25 2021 at 17:01):Théo's counterexample is interesting but might not invalidate the rule... luckily this SE is Theory-B only.
Paolo Giarrusso (Nov 25 2021 at 17:02):@Karl Palmskog I'd vote to reopen, and have some reputation on TCS.
Paolo Giarrusso (Nov 25 2021 at 17:03):I haven't been there in a while, but I don't think that problem is insurmountable.
Karl Palmskog (Nov 25 2021 at 17:03):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.
Karl Palmskog (Nov 25 2021 at 17:14):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: Oct 13 2024 at 01:02 UTC