[Agda] Hanging out with the Lean crowd

[Nicolai Kraus]

Thanks for the interesting observations!

My impression is that Agda is used a lot for computer science / 
programming language research, while Lean is
used for formalising mathematics (obviously with many many excpetions). 
These are different although certainly overlapping communities. As a 
result, Lean has huge libraries of formalised (in Kevin Buzzard's words) 
generic mathematics, and Agda has many developments which study the 
meta-theory of type systems, and so on. In principle, both communities 
could use the same system, I guess it has happened for "soft" reasons 
(social reasons, "marketing", random chance etc) that they don't. I 
don't know whether Lean is fundamentally better than Agda for 
formalising maths, or whether Agda is fundamentally better than Lean for 
PL research. Probably not, but I also don't think there is any problem.

The above is just what I have observed, I don't want to suggest anything 
since I think it's very good already :-)
(I agree with the single communication system though, that would 
probably simplify things.)

Nicolai



On 20/08/2020 17:38, Carette, Jacques wrote:
>
> No, I’m not leaving Agda. I have invested too much time already, and I 
> really do like it very much. I am/was incredibly curious as to what 
> seems to make Lean more of a ‘rising star’.
>
> My personal conclusions:
> - it’s not really the system per se, although Lean being ‘classical’ 
> helps attract a different crowd,
> - it’s the **ecosystem**, and in particular,
> - the large, extremely active and welcoming crowd of **math-lib** 
> developers that make Lean so attractive.
>
> The visible face of Lean is not Leonardo, but a large number of the 
> library developers. They’ve taken to github and Zulip with a 
> vengeance. There can be 200-300 messages/day (!) on the Lean Zulip. 
> [That’s kind of exhausting… but I guess that’s the price of success.]  
> Where there are 18 open PRs on agda-stdlib (with the latest as #1279), 
> there are currently 77 on mathlib (latest #3879).
>
> The good news for the Agda devs is that the “system devs” of Lean are 
> basically not visible here. They exist, are very busy doing cool 
> stuff, but the community is not run by them at all. Frees the system 
> devs to focus on their core strengths.
>
> My take homes, if the plan is to continuing growing the “Agda ecosystem”:
> - the community ought to pick a single communication system (Slack, 
> Discord, Zulip, gitter, whatever, but just one!)
> - the merge-into-stdlib process needs more bandwidth (Matthew’s done 
> an amazing job, I’m mostly suggesting that he make proposals as to how 
> to scale up)
> - actively push people who have useful private libraries to submit 
> them (perhaps in pieces) to stdlib
>
> For example, there is quite a lot of PL meta-theory ‘out there’, in 
> Agda. It could make a lot of sense to augment stdlib with the standard 
> material for that. Lean’s math-lib is driven by formalizing “regular 
> math” (their terminology, not mine). To me, it would make sense if 
> Agda’s stdlib was driven by “the math+CS that its users regularly 
> use”. [Thus PL meta-theory as an obvious example.]
>
> Jacques
>
> PS: there is not an iota of complaint in the above. It is 100% meant 
> as conveying my observations, and personal conclusions on how to build 
> momentum.
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

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