[Agda] Hanging out with the Lean crowd

Jorge Blázquez Saborido don at jorgebs.es
Fri Aug 21 19:18:34 CEST 2020


Hi all,

I'm an undergraduate student on Computer Science and, inspired by Kevin 
Buzzard, I started formalizing parts of the Theory of Computation. 
Since I have experience with Haskell, and Lean seems more of a tool for 
mathematicians, I chose Agda. I also chose Cubical Agda, since it looks 
very promising. If you plan on doing some kind of big project 
formalizing CS in Agda, I would be very interested!

I think having some repositories that are maintained by the community 
would be greatly beneficial. I often find projects in Agda but they are 
either very old or incompatible. I don't think we should necessarily 
follow Lean's mathlib monolithic style. We can maybe have 5 repos in 
the Agda community's GitHub, each for a different branch of CS/maths.

Regards,

Jorge Blázquez Saborido

P.S.: here is the link to my repo formalizing theory of computation: 
<https://github.com/jorge-jbs/theory-of-computation>


El vie, 21 de ago de 2020 a las 17:47, James Wood 
<james.wood.100 at strath.ac.uk> escribió:
> 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 <mailto:Agda at lists.chalmers.se>
>>>  <https://lists.chalmers.se/mailman/listinfo/agda>
>> 
>> 
>>  _______________________________________________
>>  Agda mailing list
>>  Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>  <https://lists.chalmers.se/mailman/listinfo/agda>
>> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se <mailto: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/20200821/edb5c559/attachment.html>


More information about the Agda mailing list