31

Note: I am not sure I am using the Area 51 discussions correctly in the sense that I am not asking a SE-style question. This is rather an opinion on why I am proposing a new site. Please feel free to tell me off and I'll delete this. In fact, is there the correct place to post rationale for a new site?

It may look like the needs of people who develop and use proof assistants are already met by the very active Zulip instances (Lean Zulip, Coq Zulip, Agda Zulip, Isabelle Zulip). While these are indeed very active, I believe an SO site would serve a different, but equally valuable purpose:

  • StackExchange excels at organizing knowledge. If you look at the Zulip chats, you will see that they are not very structured. For instance, in Lean almost all discussions take place on #general.
  • StackExchange is searchable a lot more easily than the Zulip chats.
  • StackExchange is more visible.
  • Last but not least, a single proof assistants StackExchange site will bring all the communities together.

Proposal: Proof assistants

4
  • 2
    What URL of the site do you suggest? proof-assistant seems too long to me.
    – ice1000
    Nov 19 at 22:44
  • I haven't thought about it. I expect SE has an established procedure. Nov 19 at 23:55
  • 3
    qed.stackexchange.com might be a good option (alludes to Ringer et al.'s survey as well).
    – k4rtik
    Nov 20 at 20:19
  • Once I suggested to create a Computational Logic Stack Exchange site but it was not welcome by some theorem prover expert. Nice to see this recurring.
    – Gergely
    Nov 23 at 9:32
20

As this answer (sorry for the shameless self-promotion) suggests, there are many people asking proof-assistants relevant questions on various SE sites, including StackOverflow, CS, TCS, etc. which means none of these sites seem to be good enough to unite everybody. The number of questions is not small.

A specific site about proof assistants will help with the status quo.

This is also the practice of other SE sites. Consider Game Development, which is a site mostly about programming in a specific area (I know Game Development itself is not only about programming, I'm talking about the SE site only), so it looks like a subset of StackOverflow. However, Game Development is thriving as an individual site. This could also happen to Proof Assistants.

17

[I've just mentioned this as a comment on another answer but I think it fits well here as an answer.]

Over the summer it became apparent that I'd be teaching a Lean course to mathematicians during this academic year. In particular I was suddenly in charge of teaching undergraduates a programming language (something I'd never done before!). I started asking a bunch of undergraduates (not just mathematicians, but computer scientists and physicists etc -- two of my kids are undergraduates right now so I had a nice source of guinea-pigs) how they learnt programming languages. The response seemed to be universal -- they tended not to even look at the resources which were provided to them, they just went for it, and if they got stuck then they googled the error.

Right now the big problem with the multi-Zulip system is that Google Doesn't Work. The good stuff is behind a login-wall, and the random mirrors that people set up are mostly ranked lowly by search engines and also non-interactive -- you can't add a comment that you are a beginner and this was helpful, i.e. the upvote.

I think that right now the whole proof assistant community is in a position where it has the potential to really grow. There have been articles in Nature, Quanta and elsewhere recently, and there's more to come. But for this growth to happen it's essential that young people get involved, and these people are not necessarily creating accounts at lots of Zulip instances but they are googling for answers and they might well have a login on the SE network because it covers many many things nowadays, so they're more likely to be able to comment or upvote things which helped them in a hassle-free way.

You know that dumb git question which has 1000 upvotes on an SE website because people keep making the same mistake and the software is hard to use? Well that's us as well.

2
  • 1
    That was enjoyable, thanks.
    – Guy Coder
    Nov 21 at 14:37
  • This was mentioned on Hacker News and relevant. Googling for Software Development: What Developers Search For and What They Find (pdf) Thought you might like it.
    – Guy Coder
    2 days ago
6

It may not make much difference for those (few?) who are already engaged in a community that uses instant messages to communicate. But SE sites have the potential to make the subject (and its troubleshooting) more popular and accessible. Being able to find open discussions about it just by typing it out in some search engine is a true gift IMO.

4

Being a long time an active member of StackExchange sites here are some of my thoughts and added information that might be of value.

  1. StackExchange sites focus on objective questions and answers and have an ethos unlike many other sites. The ethos is that questions need to be objective and sites have a currency based on votes which IMO is harmful.

  2. The culture of a StackExchange site will have a large impact on people who rely on search engines for learning. By this I mean that StackExchange site Q&A tend to get higher rankings in Google and those learning will look at answers posted for learning. Thus people new to an area tend to get their first taste of a community from the StackExchange sites. Thus those that are active on such a site can have a large impact on the outward appearance of such a community. This can be a good or bad thing and only time will tell.

With regards to

StackExchange excels at organizing knowledge.

I have to fully disagree with that. For some sites, maybe, for some tags on some sites that have a subculture for that tag, maybe, but in general I see that the sites generate more noise than signal.

When StackExchange experimented with documentation (ref) it was a great move toward organizing knowledge but SE abandoned the experiment.

If you look at the Zulip chats, you will see that they are not very structured.

I think the reply to this is obvious, they are chat sites not textbooks. I would not expect the information to be well organized.

StackExchange is searchable a lot more easily than the Zulip chats.

Searchable yes, useful results, that is a hit or miss.

One of the StackOverflow tags I visit daily is the Prolog tag. Many learning Prolog start off learning about list and so ask questions about list. The problem with relation to StackExchange (SE) is that many students use the site and teachers keep giving different problems needing the same basic understanding. Since the students either don't realize this or are to lazy to do basic search (research) they just post a question and wait for the answer. A few days ago I did a search of the Prolog tag with answers containing the word list and found 7,858 results. If we change the word list to the tag list [list] there are still 3,210 results.

To further the problem, the Prolog tag is not a vary popular tag on StackOverflow (SO), applying the same for JavaScript is even worse. Searching the JavaScript tag for function returns 1,647,310 results

StackExchange is more visible.

As I noted earlier that is true because Google gives SE sites a boost for page ranking. But as I also noted earlier, the site then becomes one of the main welcome mats to the community and that can be a good or bad thing. Since SE sites have some pretty serious constraints those constraints distort the true liveliness of the community.

  1. When looking at the points (used as a correlation of being new to SE) of recent followers the number of people with low counts I have to ask if this really a tool that they should have in their toolbox? As @Andrej notes

the very active Zulip instances (Lean Zulip, Coq Zulip, Agda Zulip, Isabelle Zulip)

there are already useful tools one can add to their tool box.

  1. Another major problem with SE answers is that people new to a tag, e.g. JavaScript, may not know that the accepted answer is not the answer they need. They may not know that the answer was good back then but is now a wrong answer. They may not know that the right answer by the expert in the field was given but because users are fungible to them they can't discriminate. They may not know that the correct answer was given in a comment. That the correct answer may be posted in a discussion. That the correct answer may be in a link given.

  2. SE sites require one to earn points to gain privileges. Does the community for proof assistants need a gaming system to help in learning?

Having spent years on these SE sites one of the odd things one learns is that some of the most basic and easy questions earn the most points and some of the more advanced and time consuming answers get next to no points. Where is the physics in that?

  1. SE sites all have moderators. The moderators can have a significant impact on the direction of a site and thus one of the welcome mats for the community. So if and when the site goes live, think seriously about who you would want to be the moderator. I am a admin with full moderator privileges for a Discourse site and while I have learned a lot from the experiences, it is not a privilege that should be granted lightly.

  2. Some teachers forbid their students from using SE sites so the students create burn accounts (think burner phone) to ask the question. After the question is correctly answered they delete the question and thus it deletes the answer and the information is lost. This happens more often than many know.


In fact, is there the correct place to post rationale for a new site?

Many years ago I use to be active on this site (Area 51) so yes the Area 51 meta site is the correct place to post this. The other way to think about it is, where else would it go? There is no where else, this is the logical place. :)


I have quite the respect for @Andrej and even noted that one of his answers was the most useful information I have ever received in a SE answer. (ref) Also some of his code is the quite useful. (ref)

19
  • 3
    I hope I am able to distinguish a critique of a proposal I made and me as a person :-) Regarding the influence an SE site has on the culture, I completely agree that much depends on how beginners are received, and how welcoming the community is. Community sites undergo an evolution from initial enthusiams and openess to an established hierachy with cultural norms. Consider Wikipedia, for example. I do not know how to "fight" against it, but I suspect Zulip chats are not immune to the problem either. Nov 20 at 9:43
  • @AndrejBauer It was not meant as personal expect for the respect at the end. If there is any part that hints as that I will gladly change the wording. :)
    – Guy Coder
    Nov 20 at 9:48
  • @AndrejBauer If this site needs moderators will you be tossing your hat in the ring?
    – Guy Coder
    Nov 20 at 9:55
  • I have downvoted this answer to indicate my disagreement with many of your conclusions. Nonetheless, I thank you for the effort that you have made to lay out this point of view. Nov 20 at 10:12
  • @NeilStrickland Thanks for the honesty. I fully expected this to get many downvotes and being a long time user of SE meta sites take the down vote to mean you disagree with the information and not the person. :)
    – Guy Coder
    Nov 20 at 10:15
  • @GuyCoder: only if you're not throwing in the towel. Nov 20 at 21:12
  • @AndrejBauer I don't plan on it. But if the site needs me to fill in one of the slots then I guess I could toss may hat in. :-)
    – Guy Coder
    Nov 20 at 21:16
  • @AndrejBauer Did you notice that Wheat Wizard is committed and a moderator at Code Golf?!
    – Guy Coder
    Nov 20 at 23:10
  • Are we impressed? Sorry about my ignorance. Nov 20 at 23:22
  • @AndrejBauer I don't get what you mean. If you are asking if I am impressed with how popular and fast the site is gaining traction, then yes this is very impressive.
    – Guy Coder
    Nov 20 at 23:25
  • I am displaying my own ignorance about who Wheat Wizard is. Are we impressed as a community that he's here? Nov 20 at 23:51
  • 1
    @AndrejBauer Oh. Thanks for the clarification. The reason I noted him is that being a moderator on another StackExchange site, he would probably be of help in setting the right tone if and when the site goes live. He might even want to be a moderator for this site.
    – Guy Coder
    Nov 21 at 0:12
  • I don't have much stake in the proof-assistant site, but I don't get the goal of this answer. It seems to argue against the existence of SE in general more so than this specific proposal.
    – Tyberius
    Nov 21 at 0:32
  • @Tyberius You did not read it wrong. The context in which I wrote the so called answer was added information that might be of value. Having been programming since the days of key punch machines I have seen many things presented with just the positives. It is also nice to get the negatives so one can make an objective decision. Thus the information is pointing out where the mines in the minefield are. continued.
    – Guy Coder
    Nov 21 at 0:39
  • 1
    @GuyCoder okay that makes more sense, you are just warning that "the grass isn't always greener" which is good to keep in mind. The newish site I'm a mod for has definitely had to do a lot of to get new users to understand how SE works.
    – Tyberius
    Nov 21 at 14:17

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .