Hi folks, last Friday Lean held its first FRO community meeting; I found it very interesting. I took notes, but both slides and video are public, so if you are interested on it, you can go and watch by yourself!
https://www.youtube.com/watch?v=jaibFnoMDSw
What is Lean FRO? I've seen this acronym pop up everywhere without any associated explanation.
@Théo Zimmermann is a new kind of organization, see https://www.convergentresearch.org/
and the video
There are many details, but the basic idea is that they are a new organization system "focused research org" in order to do research that doesn't fit well in academia or industry
exactly the kind of work Lean or Coq need to do IMO
The idea is to build a focused knit-tight team, that closely collaborate; IMHO that's a valid way to address the challenges the development of systems like Coq.
As I said I took many notes and my own intepretation for Coq, in fact after attending that meeting I rewrote my roadmap notes totally; so for now I'll go and finish my part of the roadmap PR; I think that Lean is 99% on the right track, in particular they have a very good understanding of what the key relevant points for a modern theorem prover are.
I think a few low-level technical details may prove to be not the best choice, but IMHO that's very minor
OK, interesting. And finally Leo de Moura embraces his mathematician users officially.
this is not just interesting, this is somewhat threatening for us :) lean is on track to surpass coq in terms of number of users
lean is making so many right decisions. our moat is drying up...
the whole "FRO" thing is very vaguely documented, but legally it seems to be just a US 501(c)(3) nonprofit that expires within 5 years. I don't see how it could work or make sense in a European context.
It's definitely a very American thing. And even a very American way of thinking. Still, it might produce interesting results.
Huỳnh Trần Khanh said:
this is not just interesting, this is somewhat threatening for us :smile: lean is on track to surpass coq in terms of number of users
I honestly believe that this is already the case, even though that's a very hard thing to measure. But then, there are users and users, so just having a count wouldn't even result in a fair comparison. That being said, I do not view the growth of Lean as an existential threat to Coq. I don't think that Lean success necessarily means Coq's failure, especially in a world where currently proof assistants have a lot of room to grow, next to each other, because their communities are all way smaller than what they could be. The popularity of Lean among mathematicians so far has not resulted in mathematicians hearing less about Coq, probably the opposite (granted, in the beginning of Lean's popularity growth, there was some bad press about Coq, but this is more or less over).
I think the survey provided some evidence that Lean and Coq audiences/users are quite disparate at this point (CS math vs. math math). I'm personally fine with Coq serving the CS math audience
Indeed Théo Lean could be an existential treat to Coq or not.
IMVHO given the way things are going, in the not so far future, there will be few reasons left to choose Coq over Lean.
to give some perspective: the CakeML language + compiler is such a "killer app" that it likely singlehandedly keeps HOL4 alive (30+ year old code on a "dead" language, SML)
If Coq is aiming to reach the status of HOL4 then that kinda proves the point.
It won't be long until Lean gets a port of CakeML
Or something similar (maybe their own ML-like language)
the point was more that applications of ITP can be extremely transformative, and will likely determine success in long term
there are specific properties of HOL4 that made CakeML possible (bootstrappable), the closest analogue might be Coq + Iris. Can't be ported easily.
one of the obvious problems with FROs seems to be: if you get hired by one, you are guaranteed to have to find a new job soon
Once again, we shouldn't feel threatened, we should feel hopeful that proof assistants are booming. If Lean actually ends up being the killer proof assistant that everyone uses (I strongly doubt it), then this means that it will have everything that everyone is asking for, so that will be a great achievement that we should celebrate. But the more realistic course of action is that competition will continue, because diversity actually brings what a single system cannot: adaptation to a larger range of use cases.
Karl Palmskog said:
one of the obvious problems with FROs seems to be: if you get hired by one, you are guaranteed to have to find a new job soon
How so? FRO can become self-sufficient, and then move to a proper org
Théo Zimmermann said:
Once again, we shouldn't feel threatened, we should feel hopeful that proof assistants are booming. If Lean actually ends up being the killer proof assistant that everyone uses (I strongly doubt it), then this means that it will have everything that everyone is asking for, so that will be a great achievement that we should celebrate. But the more realistic course of action is that competition will continue, because diversity actually brings what a single system cannot: adaptation to a larger range of use cases.
I understand your point Théo, but in this case there is too much overlap, and too much overlap has usually very interesting implications in psicology and sociology.
For me the question is different, as a researcher why should I use Coq to develop my techniques and papers, if using Lean I can progress much faster, thus doing better in my career?
That's a second order effect not to be underestimated
The diversity point for Coq / Lean fails IMO: they are too similar
So as of today, for me is about incentives; Coq is ahead in some areas, Lean is in others. But for how long?
"Language lock-in" is becoming a thing of the past
In particular for systems like Coq and Lean which are basically almost the same programming lang.
As I researcher, when I recommend Coq to students or colleagues, my recommendation has to be based on my own assessment of the systems, and try to pick the best for this case.
the whole point of FRO is that they close down in 5 years or less. Employees are not guaranteed to be offered opportunities elsewhere (at least nothing in the FRO structure says they will)
w.r.t. language lock-in: I think it's a hard to argue something like this, which makes use of specific features of a system to achieve something, is easy to recreate in a setting without those features. CakeML+HOL4 is the same.
I am not sure what will exactly come after the FRO, but if you look at the video, the plan for them is to become "self-sufficient". I understand this a plan to transition to some kind of Lean foundation. But indeed, this was just a guess from what I understood in the talk.
I've double checked the talk and indeed their plan is to become a foundation after the 5 years of FRO
So most employees of the FRO should be able to transition to the foundation. Makes indeed sense, otherwise it would be silly to invest in Lean if you are gonna lose your job.
is it basically true that lean is more of a math product and coq is more of a software product? that's what it's seemed like to me--- isn't it plausible that mathematicians totally bail on coq but something like VST never gets anywhere in Lean?
I commented up a google doc for convergent several months ago about this--- they at the time wanted it to have externalities on ML (specifically Dalrymple's "Open Agency Architecture" protocol/schema, which the UK government ended up liking a lot), and I recommended against getting their hopes up about that application and that coq is a better fit if they really want that, but told them as a more generic science/innovation play it makes a ton of sense
I am unfamiliar with Lean and so I am missing out on some important things here.
What are the strong technical reasons why some people think Lean is poised to eclipse Coq?
I see social and cultural reasons - Lean is very popular in mathematics now and will naturally continue to gain popularity.
I will state what I understand about the commonalities and differences between Coq and Lean and I would be grateful if anybody contributes the most salient points I am missing.
Now there are cultural differences.
@Emilio Jesús Gallego Arias Do you have any comments? For example I am under the impression that Lean's Z3 integration is not leaps and bounds better than what you could do with Coqhammer or Snipe,
unless they have somehow magically made huge leaps in the problem of how to reduce term construction in CiC to problems for SMT solvers. What do they have that is that much better? And if it is better, can it be copied in Coq?
Lean's Z3 integration simply doesn't exist
you must've misread something
Sounds that way, my mistake.
lean has a package manager and build system that's familiar to those already familiar with npm and cargo. lean's editor experience is leaps and bounds better than what coq has to offer, even though the widgets aren't a very brilliant idea. lean's object file format is portable across platforms, whereas coq object files are even dependent on the specific compiler compiling a given coq version. some lean users who have tried out coq claim that coq syntax is disgusting, but I can't relate to them though
On a factual point:
Lean has quotient types, which breaks subject reduction. Coq does not; users work with setoids
I would put this also as a cultural difference. It is easy to axiomatize quotients (as reported e.g. here), and in some cases to construct them, if one needs them.
(personal opinion) Coq should not feel "threatened" by Lean, but it should definitely recognize that it is being challenged, more than it does today. I am very skeptical about Lean and Coq being different enough that they address different use cases. The risk is that in 10 years, Coq's only users could be because of compatibility reasons on large legacy code bases. Of course this is not a fatality, but it should not be forgotten that cultural differences tend to matter more than technical differences, in the software industry. It seems critical that Coq improves at communicating a vision of what it is aiming for in the next 5 years, so that users can relate to the prroject and the community can regain momentum. This task includes converging on a roadmap but goes beyond that (communication, launch of community-driven efforts à la mathlib, etc). I believe that if needed, it should temporarily have priority over the current ongoing technical work that is ineffective due to its lack of focus.
Lean has quotient types, which breaks subject reduction
quotients don't break SR, they break canonicity
is there really need for a singular vision? The good thing about a roadmap is that it can be about a lot of things, not necessarily cohesive or unifying
Lean has definitional UIP for propositions. This breaks decidability of definitional equivalence
Lean also has Acc (accessibility predicate, used for well founded induction) in Prop, with the same effect.
Also I don't think I've seen a proof the conversion is undecidable with definitional UIP, just that the usual algorithm doesn't decide it (there is a proof for Acc making it undecidable though).
Also there are people working on a type theory with definitional uip and decidable conversion https://www.youtube.com/watch?v=9VN-4DTPSHM https://inria.hal.science/hal-03367052/ which we may get in Coq someday
SProp has definitional UIP for a special class of propositions for which this is safe
Definitional UIP "for a class of propositions" does not make sense, propositions have trivial equality. It would be "for a class of types".
SProp does not have definitional UIP by default, it can be enabled with an option for those who accept breaking conversion. It is suspected that restricting it to some types such as nat would be fine but I don't think there's a proof.
Both Coq and Lean are tactic-based. Both support reflective programming to some degree, but my impression is that Lean is the most common language to write Lean tactics
I would not say that "reflective programming" is just about writing tactics in the object language, IMO it's about producing a proof term which amounts to "this term reduces to the right thing (typically true
)". What method was used to produce the proof term (writing it by hand, tactics, typeclasses...) is not relevant to it being reflective proof.
Karl Palmskog said:
is there really need for a singular vision? The good thing about a roadmap is that it can be about a lot of things, not necessarily cohesive or unifying
Not a singular use case, but a singular vision for the project (which can evolve over time, of course), I do believe so. Doing "a lot of things" in an unstructured way tends to look like doing nothing really. A unified vision makes it easier to engage users and build actual team work (as opposed to having developers each working on their topic and synchronizing from time to time). If you look back at earlier days of the Coq project, it seems to me it had a fairly well defined and unified vision (providing a tool to build proofs in CoC and program by extraction as a new paradigm for more reliable software development). It probably needs to be refreshed today. And that takes some work.
another aspect is that "gaining momentum" might be in opposition to making life easier for existing users, e.g., something like widgets and interfaces could be flashy and bring in new users, but not clear whether they will stick around, or contribute, etc.
As to singular vision, based on research and experience I'm convinced that a lot of low-level proof engineering issues are general to most ITPs, and addressing them in a specific setting is in many cases essentially unconnected to a what that ITP is trying to do or be.
I gotta admit even on the program extraction front Lean is starting to do better than us
https://github.com/kmill/lean4-raytracer
Gaëtan Gilbert said:
I would not say that "reflective programming" is just about writing tactics in the object language, IMO it's about producing a proof term which amounts to "this term reduces to the right thing (typically
true
)". What method was used to produce the proof term (writing it by hand, tactics, typeclasses...) is not relevant to it being reflective proof.
Yes and no. "Reflection" is about the ability to manipulate and reason about the syntax of the objects in the language of the objects. So, writing a tactic in the logic is not sufficient to get reflection (that is only the "manipulate" part), you would also need to be able to prove a theorem about that tactic (or at least part of it, e.g., an a posteriori checker). And when there is a reduction to "true" (or anything else) somewhere, "reflection" becomes "computational reflection".
Huỳnh Trần Khanh said:
I gotta admit even on the program extraction front Lean is starting to do better than us
Extraction is a good example, yes. It is very hard to organize and bring some engineering resources on that topic (which are very much needed) with no unified vision of how the Coq team would like programming in Coq to look like in 5 years.
Huỳnh Trần Khanh said:
editor experience is leaps and bounds better than what Coq has to offer.
That's helpful. Can you give one or two examples
semantic syntax highlighting, that is the code is parsed into an AST and is highlighted according to the meaning in the AST. goals are updated continuously as you type, and you have the option to pause updates as you wish. there's also autocomplete. the infoview is interactive, and you can hover over individual terms and click on them to see the actual type
but actually we've made good progress on the editing experience, it's just that there are still stability issues. right now folks still prefer vscoq1 over vscoq2/coq-lsp because of stability
neither coq-lsp nor vscoq2 has semantic syntax highlighting though
ah yeah I forgot this. when you edit one file and switch to another file, in Coq you have to rebuild the whole project manually, then close the editor and reopen it. in lean you can just run "Refresh File Dependencies"
The remark of @Huỳnh Trần Khanh on portability of the object file format is perhaps true, but I don't think that's a relevant bonus point.
it is relevant though. especially if coq were to have a large scale collaborative project like mathlib. building such a project could easily take hours. object file portability means we can download prebuilt object files off of a server and get up and running
the Coq platform builds in 30 minutes overall so one wonders what's up with mathlib (and indeed, it seems Lean 3 was very slow sometimes), but the point stands
we _have_ implemented what you describe at work, but that requires downloading Docker containers with byte-for-byte identical Coq binaries
the reason for the binary format thing is basically that Coq uses OCaml's Marshal module, which is simple [at least to use] and fast. If an independent binary format is to be provided, this may require extensive discussions to be reconciliated with Coq's backward compat policy. To my knowledge, Lean has not committed to any backward compatibility yet, source or binary
but Coq doesn't have a binary backward compat policy, right?
no, but that would inevitably be on the table if a fixed format is to be provided
for example, Linux distributions apparently break binary APIs all the time, since they find it convenient. One can guess that binary compatibility takes significant resources to provide.
I think we are way paranoid with our restrictions on binary files
They do need the same Coq commit but I don't think the version of the ocaml compiler or anything else matters
empirically, rebuilding the same Coq version on the same compiler breaks compatibility IME. One reason is the lack of Coq reproducible builds, but I'm not sure that's everything.
I think what Gaëtan is saying is that Coq could relax some checks of what "breaking" means
and it may still work out with the same .vo
files from different OCaml compilers
The check is there mostly so that we don't try to link OCaml plugins that were built against a different compiled version of Coq, right? The contents of the .vo itself should not care about most OCaml version changes.
I guess Lean is self-hosting enough that most projects don't need to write C plugins for Lean, and anyway people writing C plugins are fine with fewer guarantees about ABI compatibility (and furthermore C++ dependencies are probably managed by the system package manager not by Lean's package manager?)
Karl Palmskog said:
I think what Gaëtan is saying is that Coq could relax some checks of what "breaking" means
yes
Gaëtan Gilbert said:
I think we are way paranoid with our restrictions on binary files
They do need the same Coq commit but I don't think the version of the ocaml compiler or anything else matters
They do for plugins right (due to .cmx hashing) ?
Jason Gross said:
The check is there mostly so that we don't try to link OCaml plugins that were built against a different compiled version of Coq, right? The contents of the .vo itself should not care about most OCaml version changes.
vo checks aren't really useful for that
ocaml does its own check when linking plugins IIRC
Emilio Jesús Gallego Arias said:
Gaëtan Gilbert said:
I think we are way paranoid with our restrictions on binary files
They do need the same Coq commit but I don't think the version of the ocaml compiler or anything else mattersThey do for plugins right (due to .cmx hashing) ?
the cmx hashing is not checked
it's just there so that dune takes into account the transitive dependency (typically Logic.v depends on Ltac.v which uses ltac_plugin, so when ltac_plugin changes Logic.vo needs rebuilding)
Maybe folks we could move the discussion about distributed builds to its own thread?
As to keep things tidy.
That's what I mean @Gaëtan Gilbert , in my experience most problems come from OCaml checks
About the lean editor, I was told (but haven't tried it myself) that the performances are so bad that it practically limits the size of the source files to a few hundred lines, whereas proofgeneral or coqide can handle files with more than 20000 lines (not that I think that such monsters are desirable but sometimes it just makes sense to have a 1000 or 2000 lines file).
@Pierre Roux indeed their current document engine has some limitations, I don't think they are so bad tho.
They are planning to address them tho. This is another area where Coq knows how to do better, but it is still open to see if it will do better.
I know they have a plan to fix it, but the stuff is not easy so I can't say more until I see the actual concrete technical detials
@Pierre Roux Lean 3 or Lean 4? Lean 3 has severe performance problems but all of that have been fixed in Lean 4
@Huỳnh Trần Khanh there are still some open perf problems in Lean 4
but indeed in some areas it is much better
Probably 3. But even if fixed, I guess the impact on file sizes will remain visible for some time in existing code.
Other unrelated small points after looking at the slides:
@Huỳnh Trần Khanh Well, binary distributions do exist... that's why I think it's not relevant. Big open source projects do not have run-everywhere packages, but they're still successful!
early on in the slides, it's claimed that "formalized mathematics" is the focus, but a couple of slides later we get "software verification". What is the most high-profile Lean program verification project?
Arguably there is significant MathComp-related work motivated by program verification, I think the official list has quite a lot of stuff under "Programming and Algorithms"
did Lean 4's support policy change from "go away"? https://github.com/leanprover/lean4/blob/master/doc/faq.md#should-i-use-lean
To me that's relevant to project diversity, and we know they're serious about that given their Lean 3->4 breakage...
I saw Leo say he doesn't want to rewrite Lean again, which might mean improved stability, but to me that still seems a concern
per the 4.0.0 release notes: "We do not yet make promises about backwards compatibility"
I think the team openness point is quite relevant. The classic division is between "cathedral" and "bazaar", where the former typically referred to closed-source software. But there have been plenty of big open source projects using the cathedral model (arguably Isabelle is one of them). I think it's an open question whether you can even get a singular vision in the bazaar model
it was pretty clear from the slides that only FRO employees can be code owners in Lean4.
To contrast this, it would be interesting to figure out some "decentralization" measures for Coq, e.g., how many code owners are non-Inria employees, how many commits are signed off by them, etc.
Last updated: Oct 13 2024 at 01:02 UTC