Stream: Coq devs & plugin devs

Topic: Lean FRO meeting


view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 15:15):

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

view this post on Zulip Théo Zimmermann (Oct 17 2023 at 15:18):

What is Lean FRO? I've seen this acronym pop up everywhere without any associated explanation.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 15:19):

@Théo Zimmermann is a new kind of organization, see https://www.convergentresearch.org/

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 15:19):

and the video

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 15:19):

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 15:19):

exactly the kind of work Lean or Coq need to do IMO

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 15:21):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 15:22):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 15:23):

I think a few low-level technical details may prove to be not the best choice, but IMHO that's very minor

view this post on Zulip Théo Zimmermann (Oct 17 2023 at 15:24):

OK, interesting. And finally Leo de Moura embraces his mathematician users officially.

view this post on Zulip Huỳnh Trần Khanh (Oct 17 2023 at 15:31):

this is not just interesting, this is somewhat threatening for us :) lean is on track to surpass coq in terms of number of users

view this post on Zulip Huỳnh Trần Khanh (Oct 17 2023 at 15:36):

lean is making so many right decisions. our moat is drying up...

view this post on Zulip Karl Palmskog (Oct 17 2023 at 15:46):

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.

view this post on Zulip Théo Zimmermann (Oct 17 2023 at 15:47):

It's definitely a very American thing. And even a very American way of thinking. Still, it might produce interesting results.

view this post on Zulip Théo Zimmermann (Oct 17 2023 at 15:53):

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).

view this post on Zulip Karl Palmskog (Oct 17 2023 at 15:54):

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 15:55):

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.

view this post on Zulip Karl Palmskog (Oct 17 2023 at 15:59):

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)

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 16:00):

If Coq is aiming to reach the status of HOL4 then that kinda proves the point.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 16:01):

It won't be long until Lean gets a port of CakeML

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 16:01):

Or something similar (maybe their own ML-like language)

view this post on Zulip Karl Palmskog (Oct 17 2023 at 16:02):

the point was more that applications of ITP can be extremely transformative, and will likely determine success in long term

view this post on Zulip Karl Palmskog (Oct 17 2023 at 16:02):

there are specific properties of HOL4 that made CakeML possible (bootstrappable), the closest analogue might be Coq + Iris. Can't be ported easily.

view this post on Zulip Karl Palmskog (Oct 17 2023 at 16:05):

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

view this post on Zulip Théo Zimmermann (Oct 17 2023 at 16:09):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 16:12):

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 16:13):

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?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 16:14):

That's a second order effect not to be underestimated

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 16:14):

The diversity point for Coq / Lean fails IMO: they are too similar

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 16:14):

So as of today, for me is about incentives; Coq is ahead in some areas, Lean is in others. But for how long?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 16:15):

"Language lock-in" is becoming a thing of the past

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 16:15):

In particular for systems like Coq and Lean which are basically almost the same programming lang.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 16:18):

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.

view this post on Zulip Karl Palmskog (Oct 17 2023 at 16:44):

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)

view this post on Zulip Karl Palmskog (Oct 17 2023 at 16:54):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 21:11):

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.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 21:15):

I've double checked the talk and indeed their plan is to become a foundation after the 5 years of FRO

view this post on Zulip Emilio Jesús Gallego Arias (Oct 17 2023 at 21:16):

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.

view this post on Zulip Quinn (Oct 17 2023 at 21:25):

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?

view this post on Zulip Quinn (Oct 17 2023 at 21:29):

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

view this post on Zulip Patrick Nicodemus (Oct 18 2023 at 03:45):

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?

view this post on Zulip Huỳnh Trần Khanh (Oct 18 2023 at 03:46):

Lean's Z3 integration simply doesn't exist

view this post on Zulip Huỳnh Trần Khanh (Oct 18 2023 at 03:47):

you must've misread something

view this post on Zulip Patrick Nicodemus (Oct 18 2023 at 03:53):

Sounds that way, my mistake.

view this post on Zulip Huỳnh Trần Khanh (Oct 18 2023 at 04:46):

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

view this post on Zulip Hugo Herbelin (Oct 18 2023 at 05:48):

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.

view this post on Zulip Maxime Dénès (Oct 18 2023 at 06:13):

(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.

view this post on Zulip Gaëtan Gilbert (Oct 18 2023 at 08:08):

Lean has quotient types, which breaks subject reduction

quotients don't break SR, they break canonicity

view this post on Zulip Karl Palmskog (Oct 18 2023 at 08:16):

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

view this post on Zulip Gaëtan Gilbert (Oct 18 2023 at 08:27):

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.

view this post on Zulip Maxime Dénès (Oct 18 2023 at 08:29):

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.

view this post on Zulip Karl Palmskog (Oct 18 2023 at 08:33):

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.

view this post on Zulip Huỳnh Trần Khanh (Oct 18 2023 at 08:35):

I gotta admit even on the program extraction front Lean is starting to do better than us

view this post on Zulip Huỳnh Trần Khanh (Oct 18 2023 at 08:37):

https://github.com/kmill/lean4-raytracer

view this post on Zulip Guillaume Melquiond (Oct 18 2023 at 08:40):

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".

view this post on Zulip Maxime Dénès (Oct 18 2023 at 08:40):

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.

view this post on Zulip Patrick Nicodemus (Oct 18 2023 at 12:07):

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

view this post on Zulip Huỳnh Trần Khanh (Oct 18 2023 at 12:45):

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

view this post on Zulip Huỳnh Trần Khanh (Oct 18 2023 at 12:47):

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

view this post on Zulip Huỳnh Trần Khanh (Oct 18 2023 at 12:47):

neither coq-lsp nor vscoq2 has semantic syntax highlighting though

view this post on Zulip Huỳnh Trần Khanh (Oct 18 2023 at 12:56):

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"

view this post on Zulip Julien Puydt (Oct 18 2023 at 13:02):

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.

view this post on Zulip Huỳnh Trần Khanh (Oct 18 2023 at 13:06):

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

view this post on Zulip Paolo Giarrusso (Oct 18 2023 at 13:39):

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

view this post on Zulip Paolo Giarrusso (Oct 18 2023 at 13:40):

we _have_ implemented what you describe at work, but that requires downloading Docker containers with byte-for-byte identical Coq binaries

view this post on Zulip Karl Palmskog (Oct 18 2023 at 13:42):

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

view this post on Zulip Paolo Giarrusso (Oct 18 2023 at 13:42):

but Coq doesn't have a binary backward compat policy, right?

view this post on Zulip Karl Palmskog (Oct 18 2023 at 13:43):

no, but that would inevitably be on the table if a fixed format is to be provided

view this post on Zulip Karl Palmskog (Oct 18 2023 at 13:44):

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.

view this post on Zulip Gaëtan Gilbert (Oct 18 2023 at 13:44):

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

view this post on Zulip Paolo Giarrusso (Oct 18 2023 at 13:48):

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.

view this post on Zulip Karl Palmskog (Oct 18 2023 at 13:50):

I think what Gaëtan is saying is that Coq could relax some checks of what "breaking" means

view this post on Zulip Karl Palmskog (Oct 18 2023 at 13:50):

and it may still work out with the same .vo files from different OCaml compilers

view this post on Zulip Jason Gross (Oct 18 2023 at 13:52):

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.

view this post on Zulip Jason Gross (Oct 18 2023 at 13:55):

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?)

view this post on Zulip Gaëtan Gilbert (Oct 18 2023 at 13:55):

Karl Palmskog said:

I think what Gaëtan is saying is that Coq could relax some checks of what "breaking" means

yes

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 13:55):

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) ?

view this post on Zulip Gaëtan Gilbert (Oct 18 2023 at 13:55):

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

view this post on Zulip Gaëtan Gilbert (Oct 18 2023 at 13:57):

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 matters

They 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)

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 13:59):

Maybe folks we could move the discussion about distributed builds to its own thread?

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 13:59):

As to keep things tidy.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 13:59):

That's what I mean @Gaëtan Gilbert , in my experience most problems come from OCaml checks

view this post on Zulip Pierre Roux (Oct 18 2023 at 14:46):

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).

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 14:48):

@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.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 14:48):

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

view this post on Zulip Huỳnh Trần Khanh (Oct 18 2023 at 14:49):

@Pierre Roux Lean 3 or Lean 4? Lean 3 has severe performance problems but all of that have been fixed in Lean 4

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 14:51):

@Huỳnh Trần Khanh there are still some open perf problems in Lean 4

view this post on Zulip Emilio Jesús Gallego Arias (Oct 18 2023 at 14:51):

but indeed in some areas it is much better

view this post on Zulip Pierre Roux (Oct 18 2023 at 14:51):

Probably 3. But even if fixed, I guess the impact on file sizes will remain visible for some time in existing code.

view this post on Zulip Pierre Roux (Oct 18 2023 at 15:04):

Other unrelated small points after looking at the slides:

view this post on Zulip Julien Puydt (Oct 18 2023 at 15:11):

@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!

view this post on Zulip Karl Palmskog (Oct 18 2023 at 15:31):

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"

view this post on Zulip Paolo Giarrusso (Oct 18 2023 at 15:33):

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...

view this post on Zulip Paolo Giarrusso (Oct 18 2023 at 15:33):

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

view this post on Zulip Karl Palmskog (Oct 18 2023 at 15:34):

per the 4.0.0 release notes: "We do not yet make promises about backwards compatibility"

view this post on Zulip Karl Palmskog (Oct 18 2023 at 15:39):

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

view this post on Zulip Karl Palmskog (Oct 19 2023 at 08:05):

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