[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