Karl Palmskog (Apr 15 2023 at 08:44): Karl Palmskog (Apr 15 2023 at 08:44):Any speculation about what this might mean for ITPs and indirectly for Coq?
Huỳnh Trần Khanh (Apr 15 2023 at 11:14):I'd just say it's a great thing for Lean. I believe AWS can provide resources for Lean to succeed, and eventually the Lean community won't be dominated by math researchers, which is the primary reason why I left
From what I learned AWS has been advocating heavily for TLA, I guess they'd spend a decent amount of resources to fund Lean development work
Paolo Giarrusso (Apr 15 2023 at 11:37):What can we learn from when they hired John Harrison?
Karl Palmskog (Apr 15 2023 at 12:24):not sure about Harrison specifically, but recall that they also have more general verification/reasoning people such as Rustan Leino and Byron Cook. There may be verification going on in the AWS backend that is not publicized.
Patrick Nicodemus (Apr 15 2023 at 20:39):AWS also develops Dafny. I went to a talk the other day where Michael Hicks presented recent work on a domain-specific language for managing security policies, Cedar. https://www.cedarpolicy.com/
Paolo Giarrusso (Apr 15 2023 at 22:37):Oh, so Rustan Leino's Dafny followed the same path, from Microsoft Research to AWS
Paolo Giarrusso (Apr 15 2023 at 22:38):Of course, this doesn't let us make strong prediction, but surely it's a data point
Patrick Nicodemus (Apr 16 2023 at 00:12):Huỳnh Trần Khanh said:
I'd just say it's a great thing for Lean. I believe AWS can provide resources for Lean to succeed, and eventually the Lean community won't be dominated by math researchers, which is the primary reason why I left
From what I learned AWS has been advocating heavily for TLA, I guess they'd spend a decent amount of resources to fund Lean development work
As a mathematician I think that Coq can hopefully be a tool which is useful to people across multiple disciplines, I hope the intended read of this is not "Thank goodness the development of Coq is not shaped by what would be useful for mathematics"
Théo Zimmermann (Apr 17 2023 at 12:49):If this can be of reassurance, the Coq developers care deeply about all users and use cases (pure mathematics, verification, and teaching) even if we are also aware that our community is made of many more computer scientists than mathematicians (confirmed by the recent survey). I also personally believe that to succeed in the long-run, a general-purpose proof assistant will need the presence of both populations.
Patrick Nicodemus (Apr 17 2023 at 14:32):@Théo Zimmermann Yes, my comment was an overreaction for sure, the math-comp library and the formalization of the four color theorem are of course more than enough evidence that the Coq team sincerely cares about both use cases.
Patrick Nicodemus (Apr 17 2023 at 14:39):Realistically what was going through my head was: I don't want Coq to get left in the dust by Lean wrt mathematics, which would happen if mathematics is not a priority. Twice in the past few months I have had conversations with people not knowledgeable about formal methods, and when I told them I am formalizing mathematics in Coq, they responded "Wouldn't Lean be better for that?" Of course I have no explanation for this, as I can't think of any high profile and charismatic individuals repeatedly making strong claims about Lean's superiority over all other theorem provers, but nevertheless it worries me somewhat haha.
Huỳnh Trần Khanh (Apr 17 2023 at 14:42):my impression is the lean community is way too focused on pure math research and folks not doing pure math are driven away. the coq community is more diverse and calmer
i made a PR to mathlib and it only got merged months after i left
Gaëtan Gilbert (Apr 17 2023 at 14:50):TBH there are PRs on Coq stdlib which take a while before there's any response too
Patrick Nicodemus (Apr 17 2023 at 15:04):Yeah this seems to be a feature of any sufficiently thin community. You have projects with a single caretaker who only comes back to check on it once in a while, academic abandonware that gets dumped when authors move onto the next paper, etc.
Théo Zimmermann (Apr 17 2023 at 15:15):I would call neither Lean's mathlib nor Coq's stdlib abandonware though :sweat_smile: :big_smile:
Stefan Monnier (Apr 17 2023 at 16:44):AFAICT Lean and Coq's underlying "core language" is very similar. Obviously, "irrelevant details" end up having an enormous impact on style, on what is idiomatic, etc... but WIBNI we had a tool that takes a library from one and "ports it" to the other?
Karl Palmskog (Apr 17 2023 at 16:49):@Stefan Monnier the Lean3-to-Coq library translation has been done: https://coq.discourse.group/t/alpha-announcement-coq-is-a-lean-typechecker/581
Gaëtan Gilbert (Apr 17 2023 at 17:05):IIRC the implementation of the translation had some issues but at least in principle Lean 3 -> Coq is possible
Lean 4 -> Coq is harder because Lean 4 added recursive primitive records, Lean 4 primitive nat optimization also presents difficulties
Coq -> Lean requires dealing with universe cumulativity somehow (Coq has it, Lean doesn't)
Guillaume Melquiond (Apr 17 2023 at 17:10):For Coq -> Lean, there is also the issue of nested fixpoints. No idea how to translate them. (Is that even possible in theory?)
Paolo Giarrusso (Apr 17 2023 at 19:59):Even if you can translate the core language, usable libraries require translating between elaborators which isn't a solved problem. OTOH hard theorems are another matter
Paolo Giarrusso (Apr 17 2023 at 20:00):@Patrick Nicodemus if people ask about Lean, my joke (and not only) would be that you're waiting for Lean 42 to finally be stable
Paolo Giarrusso (Apr 17 2023 at 20:01):Also https://leanprover.github.io/lean4/doc/faq.html#should-i-use-lean reads to me as "no"
Paolo Giarrusso (Apr 17 2023 at 20:02):to be fair, the author claimed he plans to stop rewriting Lean
Karl Palmskog (Apr 17 2023 at 20:18):wait, you mean we have to see the surface code in the system we translate to? Why wouldn't just terms suffice?
Karl Palmskog (Apr 17 2023 at 20:21):for many applications, we just care about the existence of a proof term. I personally wouldn't care much about provenance/context if some convenient constant just showed up in my database
Paolo Giarrusso (Apr 17 2023 at 20:27):If you want to translate the 4-color or Feit-Thompson theorems, sure, I'm just mentioning that translating math-comp (or mathlib) is a different matter
Paolo Giarrusso (Apr 17 2023 at 20:30):Stefan asked about translating libraries, and it's possible they actually meant it.
Paolo Giarrusso (Apr 17 2023 at 20:34):Of course this isn't a new problem, it's just FFI but with elaboration in the way; I'm not even saying it's hopeless.
James Wood (Apr 17 2023 at 20:39):I don't think you'd translate proof scripts or surface language terms, given that the corresponding core language terms are perfectly usable. What you'd be missing is name management, notations, auto hints, and basically any other information that's explicitly there to drive the elaborator.
Alex Sanchez-Stern (Apr 17 2023 at 20:41):Why do you need information to drive the elaborator when you can just export the fully elaborated terms?
Alex Sanchez-Stern (Apr 17 2023 at 20:42):If you're going to be executing the proof scripts to extract the proof terms for translating, running the elaborator too seems like fair game.
Alex Sanchez-Stern (Apr 17 2023 at 20:44):Oh but I guess you're saying that you can export the proof terms for the library, but the library also has hints to elaborate user code that are needed.
James Wood (Apr 17 2023 at 20:55):Yes, I should have been clearer.
Paolo Giarrusso (Apr 17 2023 at 23:30):I should have been clearer too. I wouldn't want to consume a translation of iris proof terms from lean, and lots of math-comp seems similar
Meven Lennon-Bertrand (Apr 18 2023 at 09:12):There is much more to a library than just theorems/proofs terms: there are all sorts of tactics/hints/notations/..., but also and importantly definitions. It's already hard enough to make different libraries in Coq to communicate because they wildly differ in how they define basic notions and set their proofs up, things would get an order of magnitude more messy trying to do this between different proofs assistants. Especially since the technology of the proof assistant has a strong impact on how you set definitions up…
Karl Palmskog (Apr 18 2023 at 09:20):again, if all you care about is the existence of a proof, some minimal translation functions/lemmas suffice. There was a case study on this for Stdlib-MathComp for program verification (VST/CompCert) in a recent paper by Appel et al., I believe
Ali Caglayan (Apr 18 2023 at 12:10):I think one of the biggest surprises for mathematicians using proof asisstants is how much software engineering matters when writing proofs. You can of course do everything in a single file, but if you are serious about proofs and reuseability you need to set up some infrastructure which pulls in a lot of ideas from software development.
Last updated: Nov 29 2023 at 21:01 UTC