[Agda] On IRC, Slack, Gitter, Discord, and Zulip (re: Hanging out with the Lean crowd)

[Jesper Louis Andersen]

On Fri, Aug 21, 2020 at 1:23 PM Jesper Cockx <Jesper at sikanda.be> wrote:

> - IRC: An open system but based on archaic technology. I'm having a hard
> time browsing the history of a channel when I'm not always connected.
>

IRC is a weapon from a more civilized age.


> - Slack: Seems to be the de facto standard for many people and we used it
> successfully during the latest Agda meeting. However, it is commercial
> software and keeping a full history is not free.
>

Slack has one big disadvantage: it silos you, and having multiple slack
systems open isn't that useful in the long run. It completely fails to
accept cross-interaction between different communities.

> - Gitter: Is well integrated with Github but feels otherwise quite
> barebones compared to Slack.
>

Skipping this one, never tried it.

> - Discord: Many features are more aimed at gamers than programmers. Some
> people used it for screensharing during the Agda meeting. It is commercial
> software and we'd have to pay for certain features
>

Discord is in many ways the spiritual successor to IRC. It allows a single
account to be a member of multiple servers, ie., the hierarchy is
Server->Channel->Message, whereas the Slack hierarchy is missing the
"Server" part.

> - Zulip: Has a nice threaded interface to conversations that can take a
> while to get used to. It is 100% open source software and is explicitly
> aimed at open source communities (https://zulipchat.com/for/open-source/).
> The HoTT community also seems to be using it quite effectively.
>

Skipping this one as well, since I've never tried it. Seems to get a lot of
traction however.
You usually want:

* Async communication, since people live all over the world and they don't
always have time, so catching up with older discussions are important.
* Low latency communication. Email is acceptable for high-latency.
* Since this is Agda: probably unicode support and also support for going
fully bazonk on notation hell should be built in.
* Threading/Topic'ing. Because they tend to form and go on a tangent.
* Ability to be part of multiple communities at the same time. Otherwise,
people end up having to make a choice, which silos people and slashes
through cross-community building.
* Search indexing which work(tm). Slack has had a long history of being
weak in this regard.


-- 
J.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200826/a405e5ed/attachment.html>