Why Agda?

Stream: new members

[Jacques Carette]

@Patrick Massot asked in a different thread:

My second question may sound polemic but I'm really curious so I hope it won't sound aggressive. Since you seem really interested in mathematics, why do you use Agda which is openly a type theory playground and programming language much more than a proof assistant (and is basically not used for maths compared to Mizar, Coq, Isabelle and Lean)?

First: I am here, on this Zulip, to learn about Lean, and from the Lean community. I will not attempt to convert anyone to my system of choice.

The question is a complex one to answer. I will give a short answer first, and then a second, longer answer (in this same thread).

Short answer: I am a very strong believer in 'programming style' and diversity in PL (and, by extension / Curry-Howard, proof assistants). I'll take a PL approach here, but it's the same for proof assistants. Most people find that there are things they'd like to say "in a program", and that in different PLs, they can say those things more or less easily. I've written programs in 25+ languages 'as a living', and can read many more than that. For some things Java seems good, but C# would be equally good, and the difference between them is purely stylistic. Same between Python and Ruby. There are differences in ecosystems, yes, but that's somewhat different (if still important). The gap in style between C and Rust, even though in some sense they both aim to fill the same niche, is much larger. And, the gap between Prolog and C++ is more like a vast chasm. I would never want to write a device driver in Prolog, but I would be quite unhappy to write a wildly backtracking knowledge-based inference engine in C (unless the efficiency really, really, _really_ mattered). [Yep, this is the short answer.] So, for the things that I want to say right now, in the ways that I like saying them, Agda fits best.

Long answer: I used to be a mathematician. My undergraduate was a joint Pure Math - Computer Science at Waterloo, a Master's degree in Pure Math at the Université de Montréal, and a Ph.D. in pure math from the Université de Paris-Sud (Adrien Douady as primary supervisor, but finished with John H. Hubbard from Cornell as my de facto co-supervisor), although I spent most of my time hanging out with Philippe Flajolet, Bruno Salvy and Frédéric Chyzak of the (now defunct) ALGO group at INRIA-Rocquencourt, working on symbolic computation stuff in Maple. Because even though I did my Ph.D. in 1993-1997, I actually also worked for Maplesoft 1991-2002. So rather than being a TA to earn a living during my PhD, I continue to work (part-time) for Maplesoft. So much easier to fix a bug in 'limit' than to prove (on paper!) a new theorem about the geometry of Julia sets! From my formal education, it seems like I'm a mathematician. But my joint CS degree was coop, so I also did work in Algol 68, code generation in Cobol (of Cobol code), hideous stuff in RBase 5000 and DBase IV, GIS work in C (yay, quad-trees and SQL query generation), as well as working on Character Windows for Lan Man (those drop shadows for menus in character windows? yep, that was me) and Presentation Manager for OS/2 at Microsoft back when not only was OS/2 a thing, but Microsoft and IBM worked together. Lots of fun there.

But I kind of pictured myself as a programmer. I did a master's mostly because I wanted to learn more about complex dynamics and I could live in Montreal while doing it, and a Ph.D. because I could learn even more from the world experts and live close to Paris while doing it. What I seem to like more is to _teach mathematics to computers_.

During my 11 years at Maplesoft, I changed from being a GUI programmer (I was hired to write the first Windows UI for Maple, back in the days of Windows 3.0, shudder), to founding the Math Group (all development use to be at Waterloo, I started the move to having it done at the company) and growing it from 2 to 12 people, to leading the whole development of one of the biggest releases, Maple 6. [Big because it was the last time there were very large breaking changes to how the language worked.] During that time, I read 100% of the bug list and about 80% of the code base, so roughly 600,000 lines of code [then!]. Careful analysis of where the bugs were definitely taught me a lot. But showing some aptitude for management was my downfall: I both thought I could "rise higher", but also wasn't really 'thinking' much anymore. I was a rather naive manager at a complex time, so I ended up driving the 40ish people working for me way too hard - and so they did not like me as a boss. So I did not get promoted by the new management (in retrospect, correctly so), but shifted sideways to various projects that needed rescuing. And rescue them I did. But I did realise that I was at a dead end. And a perfect opportunity to go to academia arose, and so I jumped.

Maple is not a statically typed language. I spent so many hours debugging, it was crazy. In academia, I first discovered OCaml. Such an improvement! Then came Haskell which was better still. It resonated with me very strongly. Not that Haskell is perfect - but so many of the things that I was interested in saying, could be said elegantly (enough) in Haskell. [Those words, _that I was interested in saying_ are extremely important. I still used hideous languages like C and Java, and almost palatable hacks like Python, when some things needed to be programmed by necessity and figuring out how to do them elegantly wasn't in the cards.]

What drove me to academia? The hubris that I thought I could build a next-generation symbolic computation system; and I was convinced that it needed two ingredients: meta-programming (the knowledge duplication in the code base was ridiculous, all in the name of efficiency), and theorem proving. Bill Farmer completely agreed, and had already been working in that direction, but from the angle of theorem proving (he was ⅓ of the system IMPS , the most computational of the systems of those days). [I could, and probably should, write a long essay about that!]

As time went on, I realized one big thing: all of the mathematics that I was interested in, was not popular in mathematics departments, but very much so in computer science departments. So I eventually relabelled myself as a computing scientist (not computer!). During that time, by working very hard at teaching math to computers, I also slowly became a constructivist. I became less and less interested in non-effective results.

Constructivity is not for me a matter of right/wrong. It is a matter of where I choose to spend my time. I choose to explore things from a constructive angle. That also led me to choose various other paths. For example, it led me to investigate (typed) meta-programming and the constructions from Universal Algebra as key tools for teaching math to computers in a way that was much more efficient with respect to human labour.

So why Agda? I like writing explicit lambda terms that inhabit my types. I like proofs in Set rather than in Prop. I like mixfix syntax. I like very powerful dependent-pattern matching. For some of my work in the meta-theory of (reversible) programming languages that happen to be proof terms for some well-known algebraic structures (semirings, but eventually categorified to weak Symmetric Rig Groupoids), that happens to work quite well. And it's a happy place to investigate proof-relevant category theory, a recent hobby of mine.

The long answer comes down to: it currently fits me very well.

But, as a system builder, one would have to be blind to not see that other systems (Lean, Idris 2 and Arend) are also on to some very powerful ideas that Agda does not currently offer. So here I am, to learn.

But I was asked a direct question, and I'm kind of a sucker for answering those!

[Kevin Buzzard]

What does lean have which Agda doesn't? Do you have any experience with Coq or Isabelle/HOL?

[Scott Morrison]

Tactics? :-)

[Patrick Massot]

Thank you for taking the time to write such a long answer! It's funny that you worked with Douady in Orsay. I'm the current head of the research group where Douady was (I see that your webpage even has a link to my group webpage). It seems to me that the short version of your answer is: what you really like are fancy programming languages and constructive mathematics, so Agda fits perfectly. I was a bit confused because my very quick glance at your paper suggested a much broader scope than constructive mathematics (which is a totally respectable but very specific area of mathematics). In any case I really hope you'll be able to build tools automatically turning software independent theory descriptions into native idiomatic code in several proof assistants.

[Jacques Carette]

@Kevin Buzzard It is quite premature for me to really report on. The only thing I am certain of is that the lean community development has more 'velocity' behind mathlib than Agda has behind stdlib.

I don't have writing experience with either Coq or Isabelle (but I have read quite a lot of both); so my experience of them is very skewed. The statement of theories and theorems in both are quite readable [for a computer scientist]. And, as we know, tactic-style proofs are largely unreadable to humans. So when I was reading the other libraries for importing things into Agda, it was very hard for me to learn much from the proofs themselves.

[Jacques Carette]

@Scott Morrison Nice try! ;) See for example http://agda.github.io/agda-stdlib/Tactic.RingSolver.html for the RingSolver tactic. There's a whole reflection infrastructure that lets users create tactics as they want. But mostly people don't, at least yet.

[Jacques Carette]

@Patrick Massot On your summary: I agree that I spend my own time on "fancy programming languages and constructive mathematics". But that misses one subtlety: I use these two things to produce mathematics _of any kind_. I've generated scientific computation code for all sorts of classical stuff, and am happy to produce theories for any foundations, in fact, I want to.

So my paper does aim to reach a much broader scope of mathematics. I'm just very careful to use constructive mathematics 'internally'.

In other words, I'm mostly doing constructive meta-mathematics, to serve as much of mathematics as possible.

[Utensil Song]

Kevin Buzzard said:

What does lean have which Agda doesn't? Do you have any experience with Coq or Isabelle/HOL?

Also wondering the answer to the opposite question: What does Agda have which Lean doesn't?

[Utensil Song]

One answer is "cross-referencing source code" like this example in Agda and this example in Coq .

[Patrick Massot]

Jacques Carette said:

I don't have writing experience with either Coq or Isabelle (but I have read quite a lot of both); so my experience of them is very skewed. The statement of theories and theorems in both are quite readable [for a computer scientist].

The crucial part of this last sentence is between brackets at the end. Interestingly, boiler-plate cutting machines could play an important role here. For instance each mathcomp (Coq's main math library) file start with a huge wall of unification hints boilerplate that will prevent any mathematicians from accessing the main content. This is much less visible in Lean's mathlib but the issue still exists.

[Reid Barton]

I recently looked at the coq-HoTT category theory library and Coq has some neat notation features that allow things like writing C -> D for the category of functors from C to D (even though -> is normally the same as Lean's ->). No type classes or unification hints, just bundled objects and notation tricks

[Patrick Massot]

And, as we know, tactic-style proofs are largely unreadable to humans. So when I was reading the other libraries for importing things into Agda, it was very hard for me to learn much from the proofs themselves.

I think this issue is very-well understood. The issue is not the use of tactics, it's the lack of powerful tactics. The ideal proof is a mostly a sequence of assertions (have or obtain in Lean`) separated by one or two lines of powerful tactic calls, not unreadable proof terms (this is the Isabelle+Sledgehammer style).

[Jacques Carette]

The wall of unification hints, to me, is two things: 1) a very technology-specific mechanism taken very far, and 2) an encoding of certain mathematical knowledge (about the structure of domain-specific proofs) in an obscure way. Coq suffers a lot from being first in a complicated domain, so the entropy of backwards compatibility (something lean has made radical decision on!) makes such gymnastics kind of bad.

[Jacques Carette]

But I think the important part is to collect enough examples to understand what knowledge is actually being encoded there - and then automation could be designed to deal with it.

[Patrick Massot]

They already have a lot of examples, and this is why they were able to start this hierarchy builder experiment.

[Jacques Carette]

Yes, and the recent opening of the Coq engine to plugins, etc. It is now much more programmable by outsiders, and people are really taking advantage of that. MetaCoq is looking great too.

[Patrick Massot]

Jacques Carette said:

In other words, I'm mostly doing constructive meta-mathematics, to serve as much of mathematics as possible.

This sounds very good, but I think you should make it clearer if you want mathematicians to get interested. The word "constructive" is a really powerful repeler, so it requires very careful explanations.

[Jacques Carette]

To be honest, I have personally given up on established mathematicians being in my 'target market'! [Not that people shouldn't try, I just will not spend any more of my own energy on that.] I am going to build tools that I think can make people much more efficient with their time, and offer them for all to use. If they want to use them, great. And I'll support them. I just won't presuppose who my users will be.

Yes, that's somewhat cynical. But my frequent partner-in-crime for all of this (Bill Farmer) is still very keen on having mathematicians as users of our joint work. So there's that!

[Jacques Carette]

I guess the other thing is, I make a very sharp distinction between "what is interesting" (way too much) and "what is interesting enough to me that I'll spend my time on it" (a much more carefully curated list that is nevertheless much too long).

[Pedro Sánchez Terraf]

Patrick Massot said:

And, as we know, tactic-style proofs are largely unreadable to humans. So when I was reading the other libraries for importing things into Agda, it was very hard for me to learn much from the proofs themselves.

I think this issue is very-well understood. The issue is not the use of tactics, it's the lack of powerful tactics. The ideal proof is a mostly a sequence of assertions (have or obtain in Lean`) separated by one or two lines of powerful tactic calls, not unreadable proof terms (this is the Isabelle+Sledgehammer style).

In the meantime --before having strong enough tactics-- there are some structuring constructions from Isabelle that I found really nice while writing proof documents there. I'm just starting with Lean, so I'm not sure if most of them are already functional here; hopefully they are imported at some point.

[Pedro Sánchez Terraf]

A very simple albeit nice one is moreover...ultimately, that allows you to accumulate intermediate "assertions" (in Isabelle we would say facts-- hope this is the correct translation) and then proceed to a conclusion. This minimizes cross-references, which can obscure the reading pace.

[Jalex Stark]

is there something you can't do with have, suffices, and focusing brances that you can do with moreover...ultimately

[Mario Carneiro]

@Pedro Sánchez Terraf By the way, your observation about moreover ... ultimately on CICM slack lead to this discussion about isabelle syntax in lean, which might be of interest to you

[Pedro Sánchez Terraf]

@Mario Carneiro a juicy thread indeed!