[Agda] Hanging out with the Lean crowd

[Martin Escardo]

>From my personal point of view, Lean has two defects:

 * It used to support HoTT/UF and it doesn't anymore.
 * It is ostensively classical and neglects constructive mathematics.

I understand that for the vast majority of people this is (seen as) an
advantage.

But not for me and the people I tend to work with.

Otherwise Lean is wonderful.

Best,
Martin

On 20/08/2020 17:38, carette at mcmaster.ca 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
> 

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe