Why have a Proof assistants SE site when there are already very active Zulip instances?

Question

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

Answer 1

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.

Answer 2

[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.

Answer 3

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.

Answer 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.

4. 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.

5. 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.

6. 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?

7. 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.

8. 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)