Email Gateway (Aug 19 2022 at 10:18): Email Gateway (Aug 19 2022 at 10:18):From: Gottfried Barrow <gottfried.barrow@gmx.com>
It's first come first serve, so I hijack a suggestion from
[isabelle-dev], to try and get my point in first:
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg03860.html
http://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg03864.html
Mentioning the general downsides to stackexchange.com are irrelevant
here because they only affect whether a person will use
stackexchange.com in general.
As I see it, there could be three wrong choices made by someone or some
people in trying to initiate the use of stackexchange for proof
assistants, ATPs, computational logic, or whatever word it is that best
categorizes these and related fields of study.
(1) People choose the wrong stackexchange site as a springboard for the
future site http://proofassistants.stackexchange.com, or whatever other
site would be broad enough to get some traffic.
(2) All competing groups don't choose to listen in on the stackexchange
site that is chosen as a springboard site. In particular, the HOL4 et
al., Mizar, Coq, Isabelle, etc. groups don't all choose to be a part of
the springboard site.
(3) Someone doesn't choose to make it practical for people to listen in
on the small number of proof assistant, etc. related questions that will
be asked on the springboard site.
Now, I give my opinions about (1), (2), and (3).
The challenge for (1) requires a list of 3 questions:
(a) On what site are the experts who have knowledge that is most closely
related to proof assistants, etc.?
(b) For that particular site, will those experts tolerate questions
about proof assistants, etc.?
(c) For that particular site, will those experts tolerate questions
about proof assistants from non-experts?
As an example, there is math.stackexchange.com, and there is
mathoverflow.net, and though mathoverflow is not a stackexchange site,
it is comparable.
On math.stackexchange.com, there are many experts in math, and they
tolerate a wide range of questions. On mathoverflow.net, there are many
experts in math, and many of those experts work to protect their domain,
to the point of keeping out advanced areas of math that overlap with
things like computer science.
I looked briefly at http://stackexchange.com/sites
1.8m users, http://stackoverflow.com/
4.9k users, computer science, http://cs.stackexchange.com/
11k users, theoretical computer science, http://cstheory.stackexchange.com/
2.6K users, computational science, http://scicomp.stackexchange.com/
The choice of a site ties (1) and (2) together, because eventually for
any user, the important questions are not just about how to use the
software, but also about the application.
Based on my observation, if I was going to pick one word to describe the
group of experts that proof assistants, etc. revolve around, it would be
"logician". So it appears to me that the experts are mainly going to
come from logicians, mathematicians, and computer scientists.
So which of those four sites has the highest concentration of logicians,
mathematicians, and computer scientists who will be tolerant in the ways
I describe above?
And to increase the size of the group of experts, you need the people I
listed in (2) listening in. Someone using Coq would be more likely to
answer certain questions of mine than someone using Isabelle, because
certain questions will be more application specific than software specific.
Finally, someone would need to make it practical for everyone to listen
in, like post a daily summary of the proof assistant, etc. questions
posted on the springboard site. I have math.stackexchange.com in my RSS
reader, but I never check what messages are retrieved. At this time, I
have only a very narrow interest, which happens to be learning how to
implement some math in Isabelle, where the math is sufficiently
explained in textbooks. I'm not going to browse the message titles
looking for something very unlikely to be there.
This daily summary email on lots of different mailing lists might make
the specific site chosen less important. But you would need a
combination of it being practical to find the pertinent, daily questions
using a search, and the people on that site would need to not be hostile
to proof assistant, etc. questions.
Regards,
GB
Email Gateway (Aug 19 2022 at 10:18):From: Serguei Mokhov <serguei@gmail.com>
Why not give a try to http://www.discourse.org/ ? Started by the same
guy as stackexchange.com/stackoverflow.com
http://www.discourse.org/about/
Email Gateway (Aug 19 2022 at 10:18):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Serguei,
I'm going to try and check out of this thread as fast as possible
because it would take people like Makarius, who have connections with
groups like the Coq group, to get things going as I described.
But, off the top of my head, I would say the reason to not use any site
other than stackexchange would be because of the momentum that
stackexchange has.
One downside to using stackexchange is that a person has to have an
account. But, discourse.org also requires a person to have an account,
so if you're looking for the most potential traffic, then you pick the
site which has the largest number of people with accounts.
The other general downside is the voting, but that's independent of all
this, and they're all going to have that, and the voting raises the
quality of questions in some ways. That's my observation. I don't have a
stackexchange or mathoverflow account.
Regards,
GB
Email Gateway (Aug 19 2022 at 10:18):From: Joachim Breitner <breitner@kit.edu>
Hi,
Am Freitag, den 22.02.2013, 10:57 -0600 schrieb Gottfried Barrow:
(2) All competing groups don't choose to listen in on the stackexchange
site that is chosen as a springboard site. In particular, the HOL4 et
al., Mizar, Coq, Isabelle, etc. groups don't all choose to be a part of
the springboard site.
there is Coq on that list, and if you include, say, Agda, then it begins
to read a bit like a list of programming languages, some with a special
purpose. That reasoning would maybe make http://stackoverflow.com/ the
right side to start on. There are already tags for some of these
provers:
http://stackoverflow.com/questions/tagged/agda
http://stackoverflow.com/questions/tagged/coq
and even
http://stackoverflow.com/questions/tagged/isabelle
so maybe we just have to spread the word that there are answers to be
gotten on SO about Isabelle?
Finally, someone would need to make it practical for everyone to
listen in,
Isn’t http://stackoverflow.com/feeds/tag/isabelle enough?
Greetings,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 10:18):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Joachim,
It's enough to put the feed in my reader.
That's an example that you can't depend on people knowing certain
things. I knew how to put a stackexchange site in my RSS reader, but
I've never even considered the idea that the tags are there to get a RSS
feed. And the nature of tags is that there can be a lot of overlap, and
people don't take the time to tag things in a way that all the
information can be found based on tags.
But even now, my motivation remains low to put any thought into
stackexchange as a meaningful source of information about Isabelle. I
see here a total of four questions that are tagged "Isabelle".
http://stackoverflow.com/questions/tagged/isabelle
If I was going to make another point in my initial email it would be this:
The people who are running these proof assistant shows will have to
promote the use of a stackexchange site for it to become, any time
soon, a hub of activity for proof assistants.
I present an analogy. If none of the proof assistant groups promoted
their mailing lists on their web sites, would very many people subscribe
to their mailing lists?
It's a common problem. To get people to jump on the bandwagon so you're
not forgotten, you have attain critical mass. You can't attain critical
mass because no one will jump on the bandwagon, which leads to everyone
totally forgetting about you, tuning you out, and turning you off, to
where you've lost any ability to get their attention, because you got
taken out of their RSS reader, or got unsubscribed to because your
channel was a dead channel.
I'll try to make this my last comment about this. Getting all this going
is way bigger than me. It's not my problem; it's just I have lots of
opinions.
People higher up on the ladder like you would have to get things rolling.
Regards,
GB
Last updated: Apr 20 2024 at 12:26 UTC