[Agda] Hanging out with the Lean crowd

[James Wood]

Hi all,

Nicolai makes good observations here. I would, though, argue that some
of the differences in focus *can* be explained by the differences
between the two systems. In particular, I both personally believe and
think it's common wisdom that Agda is the best tool for type-directed
programming, of the kind that naturally extends to
correct-by-construction programming. This is mostly due to interactive
editing of pattern-matching definitions. As far as I know, Idris is the
only comparable system in this regard (and I would mostly be happy to
write my dependently typed programs in it, too).

It happens that type-directed programming is basically what we want for
the metatheory of programming languages and logics. Usually we have two
big types – object-level types and terms – and furthermore the terms
have very careful types to enforce scoping and typing. With inductive
types with many constructors, having the constructor names appear in the
source code is useful for maintenance, and interactive editing puts them
there, rather than having to write them all out. And we really are doing
programming a lot of the time – for example, defining renaming,
substitution, and semantics.

Most other areas of maths traditionally don't resemble this
type-directed style of programming. There are few, small, inductive
types, and a lot of reasoning is done at the level of algebraic axioms
(with no inductive types in sight). These features largely nullify
Agda's advantages, and instead the advantages of Lean and Coq in the
field of proving shine through.

In summary, I think it makes more sense to view the existence of both
Agda and Lean as complementary (not to mention other systems too, with
different strengths). In particular, the two are naturally going to
attract different kinds of people. Perhaps the best we can do in terms
of marketing is to promote Agda as a view of the future of programming
(and the present of PL/logic), similar to Lean being promoted as a view
of the future of mathematics.

Maybe we can also learn, again complementarily, from Lean about how to
get things built. As I understand it, one of the main aims of Kevin
Buzzard's Xena Project is to mechanise an entire mathematics
undergraduate curriculum, and this seems to excite enough undergraduates
to make it a feasible goal. Can we do anything similar with a computer
science undergraduate programme? Could we get interested undergrads to
mechanise, say, the data structures & algorithms, logic & proof, and PL
& types courses? Would they want (analytic) cryptography theory to be
within reach? And are there areas of a maths undergrad it's worth
focusing on?

Regards,
James

On 20/08/2020 19:21, Nicolai Kraus wrote:
> 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
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>