[isabelle] stackexchange.com use for proof assistants and related software
- To: isabelle-users at cl.cam.ac.uk
- Subject: [isabelle] stackexchange.com use for proof assistants and related software
- From: Gottfried Barrow <gottfried.barrow at gmx.com>
- Date: Fri, 22 Feb 2013 10:57:53 -0600
- User-agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0
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 at mailbroy.informatik.tu-muenchen.de/msg03860.html
http://www.mail-archive.com/isabelle-dev at 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and