<div id="geary-body" dir="auto">
<p style="margin-bottom: 0cm; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: 14.000000953674316px;">Hi all,</p><p style="margin-bottom: 0cm; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: 14.000000953674316px;">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!</p><p style="margin-bottom: 0cm; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: 14.000000953674316px;">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.</p><p style="margin-bottom: 0cm; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: 14.000000953674316px;">Regards,</p><p style="margin-bottom: 0cm; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: 14.000000953674316px;">Jorge Blázquez Saborido</p><p style="margin-bottom: 0cm; font-variant-ligatures: normal; font-variant-east-asian: normal; font-variant-position: normal; line-height: 14.000000953674316px;">P.S.: here is the link to my repo formalizing theory of computation: <a href="https://github.com/jorge-jbs/theory-of-computation">https://github.com/jorge-jbs/theory-of-computation</a></p></div><div id="geary-quote" dir="auto"><br>El vie, 21 de ago de 2020 a las 17:47, James Wood <james.wood.100@strath.ac.uk> escribió:<br><blockquote type="cite"><div class="plaintext" style="white-space: pre-wrap;">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:
<blockquote> 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:
<blockquote>
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
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</blockquote>
_______________________________________________
Agda mailing list
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</blockquote>_______________________________________________
Agda mailing list
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</div></blockquote></div>