Comment by danilafe
17 hours ago
People tell me Lean is really good for functional programming. However, coming from Agda, it feels like a pretty clunky downgrade. They also tell me it's good for tactics, but I've found Coq's tactics more powerful and ergonomic. Maybe these are all baby-duck perceptions. So far, it feels like Lean's main strength isn't being the best at anything, but being decent at everything and having a huge community. I see the point and appeal, but it's saddens me that a bit of the beauty and power are lost in exchange.
In other words, it is a network effect.
My perspective is that network effects are far less long-lasting than they feel in the moment. For example if being decent at everything and having a huge community was the only thing that mattered, Perl would still be a big deal. Many similar examples exist.
In the case of Lean, being the first with a huge library really makes a difference. Just as Perl got a big boost from having CPAN. (Which was an imitation of CTAN, except for a programming language instead of TeX.)
But, based on scaling laws, we should expect the value of a large library for most users to grow around the log of the size of the library. (See https://pdodds.w3.uvm.edu/teaching/courses/2009-08UVM-300/do... for the relevant scaling laws.)
When your library is small, this looks like an insurmountable barrier. But you don't have to match the scale for factors of usability to become more important. And porting mathematical libraries is a good target for LLMs. The source is verified, the target is verifiable, and the reasoning path generally ports.
The flip side of this is that, thanks to LLMs, working on a minority platform isn't the barrier that you might expect. Because if their library can be ported to your platform, then your proof can probably be ported to their platform as well!
> The flip side of this is that, thanks to LLMs, working on a minority platform isn't the barrier that you might expect
This is a nice thought, but with Agda in particular it's just not true. It's one of the few languages I've seen that's sufficiently unrepresented in training data. Frontier LLMs (Codex, Claude Code) reliably say "I realized I can't do this." after wasting lots of tokens going back and forth.
In fact, I think this positions Agda uniquely poorly.
This. LLMs are no good at stuff they haven't seen a lot of training data for (saying this as a SystemVerilog programmer who also does some C-coding for interfacing with SystemVerilog, neither of which has a lot of open source code to show LLMs)
Huh.
I wonder how compiler technology would do. Possibly as a component of an attempted solution.
> except for a programming language instead of TeX
TeX is a programming language. It's not a very good programming language, but people have implemented floating-point math [0], regular expressions [1], an Arduino emulator [2], and terminal input/output [3] in pure TeX. The last two examples are obscure, but the first two examples are used (internally) by the vast majority of modern LaTeX documents.
[0]: https://github.com/latex3/latex3/blob/develop/l3kernel/l3fp....
[1]: https://github.com/latex3/latex3/blob/develop/l3kernel/l3reg...
[2]: https://www.ctan.org/pkg/avremu
[3]: https://www.ctan.org/pkg/reverxii
> So far, it feels like Lean's main strength isn't being the best at anything, but being decent at everything and having a huge community. I see the point and appeal, but it's saddens me that a bit of the beauty and power are lost in exchange.
To me that feels like a community that's finally matured enough to start getting on with things. Perfect tools aren't the point; get tools that are good enough and do actual work with them.
Sounds like an excuse for mediocrity.
You can apply that same argument for the of Python in the ML world. It results in all sorts of pain points that everyone has to deal with all the time.
All large-scale projects are made of mediocre parts. At some point you run out of brilliance and have to structure it so that mediocre can still be a positive contribution.
I prefer agda as proof checker but its not a practical choice for building software. Lean feels like it could legitimately become a successor to Haskell as the go to functional programming language for software development.
I think what holds Agda back from being "practical" is that it just doesn't have good tactics. You can't easily automate proofs and even simplification techniques require some language-level tricks[1]. There's technically support for elaborator reflection (as in Idris) but it's painful and impossible to debug. Certainly nowhere near where Coq and Lean are.
[1]: like this one I've used for several proofs so far: https://danilafe.com/blog/agda_expr_pattern/
Its also really slow and doesn't have a huge library ecosystem. The latter is fixable but not so much for the former.
2 replies →
I've used agda a tiny bit and Lean somewhat more, and I definitely found it much easier to write functional programs not focused on mathematical proofs in Lean than Agda. IIRC the difference was mostly tooling - Agda's documentation is kind of bad and it's a pain to get it working on your system (and it really wants you to be using Emacs specifically). Whereas Lean documents how to write the cat utility in its own docs and generally has a much better, more modern tooling experience.
I believe you, but this hasn't been my experience. It took me hours to get Lean to work (something odd was happening with the package manager + version + tooling combination). Agda worked out of the box with macOS homebrew. Agda's docs are petty bad, but I've found its cross-linked module documentation incredibly useful. The main issue is knowing something exists.
This has also been my experience with lean4.
I don't understand the forced vscode path, just let me get it as normal software in a convenient way and run it as a tool
2 replies →
I'm curious what you like about Agda functional programming? Many of the praises I hear about it have to do with it's dependent pattern matching, and I think Lean suffers a lot more in that regard. I'm curious though if you still find Agda friendlier for "normal" fp (and if so, how?)
Its parameterized modules, extremely elegant yet flexible mixfix notation mechanism, the various niceties around pattern matching (though this one might be a bit of Stockholm syndrome; Agda doesn't nicely allow pattern matching anywhere except at function clauses), the fact that records, GADTS, and modules all feel like aspects of the same thing, and the fact that typeclasses are 'just' records that are automatically filled in. The typeclass and module features IMO already give it some edge over Haskell. I don't know if it's friendlier, but it is more ergonomic.
Thanks! Typeclasses are also something I really like about Lean.
Thing is, it comes after both. Maybe it is just being a jack of all trades, but something made it success when the others remain fairly niche.
I think its pretty clear that being too early has been as bad as being too late for most technologies. There are a few that have gradually gained community after decades but it is easier to make a poor copy of one of them and have better momentum and less skepticism.
When I woke up this morning I could not have predicted someone calling a proof assistant a "Jack of all trades"
fyi it's Rocq now: https://en.wikipedia.org/wiki/Rocq
Thoughts on Idris?
Idris feels mostly dead to me at this point. Which breaks my heart, because for a split second it had real momentum around it.
Not OP, but as Haskell-derived dependently-typed languages Idris and Agda are quite similar, so I suspect if they like one they’d like the other.