# [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.
`
Regards,
GB

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*