[isabelle] stackexchange.com use for proof assistants and related software



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.