Huỳnh Trần Khanh (Jun 26 2021 at 05:15): Huỳnh Trần Khanh (Jun 26 2021 at 05:15):why should I choose lean over coq? why should I choose coq over lean? why should I choose isabelle over coq? there are several major theorem provers out there and I happen to be decently fluent in lean. can you tell me why people pick one theorem prover over another?
Huỳnh Trần Khanh (Jun 26 2021 at 05:18):and it seems that there's a lot of cross pollination among theorem provers right
Enrico Tassi (Jun 26 2021 at 05:51):If you want a technical comparison of provers this is the right place.
But the way you phrase the question is too open ended, IMO. Why do people chose Windows, Linux or OSX? Why do people chose beer or wine? I'm not kidding, it's really the same: it depends what your friends do, what the context in which you are makes more approachable. So I'm not so sure there is a precise answer to your question.
Huỳnh Trần Khanh (Jun 26 2021 at 05:58):ah so... I want a technical comparison then because I don't have much experience with other theorem provers
Enrico Tassi (Jun 26 2021 at 06:24):Help me find the right focus by telling me what you want to do. Does your domain of interest require automation? Do you need libraries (is your subject about lists and numbers or you need to rings, fields, ...)? Do you care about the bus factor (is it a research experience, or it has to last a decade)?
Enrico Tassi (Jun 26 2021 at 06:28):I like to program in ocaml for example, I'm fluent, but I would look elsewhere if I had to do system programming.
Enrico Tassi (Jun 26 2021 at 06:30):If you just want a good pick for beginners, then I would pick the one my neighbor is using, so that I can learn from him.
Théo Zimmermann (Jun 26 2021 at 06:31):Do you care about the bus factor (is it a research experience, or it has to last a decade)?
And do you care about compatibility across releases?
Huỳnh Trần Khanh (Jun 26 2021 at 08:58):And do you care about compatibility across releases?
For the time being, no.
Does your domain of interest require automation?
"require"? Well I certainly want some automation to make the proving process less laborious...
Do you need libraries (is your subject about lists and numbers or you need to rings, fields, ...)?
I want lists, numbers, inductive predicates and inductive data types. And maybe quotients. I don't need to do proper mathematics.
Do you care about the bus factor (is it a research experience, or it has to last a decade)?
The proofs don't need to last a decade. They can be irretrievably broken after a week.
Help me find the right focus by telling me what you want to do.
I want to formalize solutions to competitive programming problems on various platforms (CSES, AtCoder, etc.) The solutions need to be executable. I plan to write the solutions in WebAsssembly and prove properties about them in a theorem proving system. I think WASM is a great language to model imperative semantics. It has far less abstractions than C and C++ and because of that, it is easier to reason about WASM programs in automated theorem proving systems. Functional programming isn't good enough for competitive programming because we use a lot of low-level tricks to optimize our programs, including memory reuse, cache friendliness optimizations, recursion avoidance and other techniques.
Huỳnh Trần Khanh (Jun 26 2021 at 13:47):Alright so it seems that this question is being ignored because I'm not being specific enough. Here is a concrete question then: how does Coq's automation stack up against Lean?
Pierre-Marie Pédrot (Jun 26 2021 at 13:48):@Huỳnh Trần Khanh I am not sure that Lean is the contender for the kind of stuff you want to do.
Pierre-Marie Pédrot (Jun 26 2021 at 13:48):I'd rather look for Isabelle and/or HOL systems.
Pierre-Marie Pédrot (Jun 26 2021 at 13:49):There is a reason why everybody praises sledgehammer.
Huỳnh Trần Khanh (Jun 26 2021 at 13:51):That's a rather... unexpected response. Sledgehammer is really that good? What does it do?
Pierre-Marie Pédrot (Jun 26 2021 at 13:51):Solve all the boring stuff you don't want to do by hand.
Pierre-Marie Pédrot (Jun 26 2021 at 13:53):TBH, I don't see a big difference between Lean and Coq. They have a pretty similar design, use more or less the same foundation and the differences are probably not very relevant when compared to the difficulties one would face in all generalities.
Pierre-Marie Pédrot (Jun 26 2021 at 13:54):The only advantage I concede to Lean is the tactic language. It's hard to do worse than Ltac.
Pierre-Marie Pédrot (Jun 26 2021 at 13:55):But Lean has a lot of issues as well, in particular the fact it's not a single proof assistant. There are a lot of people stuck on Lean3 and a promise that Lean4 will wash whiter.
Pierre-Marie Pédrot (Jun 26 2021 at 13:56):It's a bit like comparing Java and C#...
Yannick Forster (Jun 26 2021 at 13:56):A relevant difference between Lean and Coq as of today is the work you can build on. For instance, since you mentioned WASM: for Coq there exists a WASM development (https://github.com/WasmCert/WasmCert-Coq), but not for Lean. Similarly, if your work is built on perfectoid spaces, you're likely better off using Lean.
Pierre-Marie Pédrot (Jun 26 2021 at 13:57):@Yannick Forster why can't I help feeling a vague sense of trolling in your comment?
Huỳnh Trần Khanh (Jun 26 2021 at 13:58):Pierre-Marie Pédrot said:
Yannick Forster why can't I help feeling a vague sense of trolling in your comment?
What do you mean? Why "trolling"? Sorry I'm new here.
Pierre-Marie Pédrot (Jun 26 2021 at 13:58):That the community that needs perfectoid spaces in their daily life can be counted on one hand?
Huỳnh Trần Khanh (Jun 26 2021 at 13:59):You are right. In fact the perfectoid spaces formalization is intended as a proof of concept—there is no math (in mathlib) that depends on it.
Huỳnh Trần Khanh (Jun 26 2021 at 13:59):So... :joy:
Yannick Forster (Jun 26 2021 at 14:00):No trolling, seriously! I chose perfectoid spaces as an example for an advanced topic. If you are interested in formalising andvanced math based on an advanced topic, you'll be happy to have some previous work there
Pierre-Marie Pédrot (Jun 26 2021 at 14:00):Well, the amount of non-formalized math that depends on them is probably of null measure so...
Yannick Forster (Jun 26 2021 at 14:02):I tried to make a general point: If you need a certified Standard ML compiler, better use HOL4 and CakeML. If you need the four color theorem, use Coq. If you need a good separation logic framework, use Coq with Iris. Sometimes, the concrete features of a proof assistant might matter less than the years of work others have done based on the (often suboptimal) features
Huỳnh Trần Khanh (Jun 26 2021 at 14:24):Pierre-Marie Pédrot said:
But Lean has a lot of issues as well, in particular the fact it's not a single proof assistant. There are a lot of people stuck on Lean3 and a promise that Lean4 will wash whiter.
Well, I'm a bit confused by your comment. Isn't Lean 3 the latest stable release and Lean 4 is not yet released? And I don't know what you mean by "wash whiter".
Enrico Tassi (Jun 26 2021 at 16:12):I think Lean4 was released last year
Enrico Tassi (Jun 26 2021 at 16:16):Pierre-Marie Pédrot said:
The only advantage I concede to Lean is the tactic language. It's hard to do worse than Ltac.
Your way to compare languages is quite funny @Pierre-Marie Pédrot , IMO you should look at what people managed to write in them as the first criteria. And even if Ltac is, well, Ltac... people did wonders with it ;-) Good \LaTeX to everybody (troll).
Gaëtan Gilbert (Jun 26 2021 at 17:15):Lean's trust story may be better than Coq. Have they had even a single proof of False yet?
Huỳnh Trần Khanh (Jun 26 2021 at 17:27):Lean? Not yet.
Huỳnh Trần Khanh (Jun 26 2021 at 17:29):Lean's type theory is equiconsistent to ZFC with a large cardinal assumption. I have a very good reason to believe ZFC is inconsistent, so a proof of false is just a matter of when not if. /s
Pierre-Marie Pédrot (Jun 26 2021 at 18:53):@Huỳnh Trần Khanh that's the official propaganda of the party, CIC enjoys the same "theorem". The sad reality is that 1. by far most soundness bugs are due to implementation issues, not theoretical issues and 2. the theory actually implemented is not the one described in those papers.
Pierre-Marie Pédrot (Jun 26 2021 at 18:53):In particular in the case of Lean there is a huge mismatch between the implementation and the theory, because Lean's underlying theory has undecidable type checking.
Pierre-Marie Pédrot (Jun 26 2021 at 18:54):@Gaëtan Gilbert maybe we try a bit more in Coq...
Bas Spitters (Jun 27 2021 at 10:13):@Pierre-Marie Pédrot I hear Ltac2 is a bit improvement over Ltac ...
Bas Spitters (Jun 27 2021 at 10:14):@Mario Carneiro might want to contribute here...
Kevin Buzzard (Jun 28 2021 at 13:58):@Andrej Bauer said in his ECM talk that if you were a mathematician interested in formalisation then he recommended starting with Lean.
Years ago I challenged the mathematics and computer science communities to begin formalising the kind of mathematics which wins all the Fields Medals, not just those in one of the corners. The odd order theorem proved we were "in" -- how many more can we get? What has become clear to me now is that the idea of having one coherent monolithic axiom-free mathematical library like the leanprover-community's mathlib, has got far more advantages than disadvantages when it comes to goals like this. Beyond some point, abstract classical pure mathematics becomes an intricately woven object, with algebra and topology and analysis all interplaying with each other (for example via number theory), and it needs to be built as a coherent whole in order to thrive. One advantage of the monolithic approach is that it gives users a "one size fits all" answer leanproject to questions like "I'm a professional algebraist/topologist/analyst/number theorist/geometer interested in formalising an API for arbitrary maths subject X, as far as I know my subject could well be classical, noncomputable and rely on all three of Lean's inbuilt axioms and furthermore I have no understanding of what that means, oh and by the way I will need to have access to an API for maths subjects A B and C, where do I start?".
I am in no position to say anything about what is the best prover for any maths/CS topic other than Fields-Medally maths. I am well aware that I have said dumb things in the past, and I've apologised for them too. I believe that this new area of formalising Fields-Medally maths could greatly benefit from attempts from groups using other systems (for example Coq, Isabelle/HOL) to emulate part or all of what we have done in Lean in a way which new users can somehow be easily led into. I recommend practicing a lot on maths undergraduates -- that's what I did. I think that it would greatly benefit this new area of formalising Fields-Medally maths if the problem were attacked by provers in the other communities.
Pierre-Marie Pédrot (Jun 28 2021 at 14:17):axiom-free mathematical library
:rolling_eyes:
Kevin Buzzard (Jun 28 2021 at 14:20)::-) We just use Lean's axioms, we don't add any new ones.
Kevin Buzzard (Jun 28 2021 at 14:21):src/ is axiom-free.
Sebastien Gouezel (Jun 28 2021 at 14:24):I guess axiom-free means here "don't pay attention to the axioms, use them as freely as an average mathematician in an average math-department would do". I.e., no problem at all with choice or LEM. My feeling on this is: if I can write a proof with or without choice, but avoiding choice (or LEM) makes it 5% harder to understand, then I'll go for choice. But I know very well that other people feel differently about this (and I won't try to convince them, contrary to Kevin :-)
Pierre-Marie Pédrot (Jun 28 2021 at 14:24):I guess it's a matter of phrasing.
Cody Roux (Jun 28 2021 at 16:01):We know your feelings Pierre-Marie :)
Enrico Tassi (Jun 28 2021 at 16:21):Pierre-Marie Pédrot said:
I guess it's a matter of phrasing.
We should add a new syntax to Coq, a synonym of Axiom, let's say Principle and all live happily ever after :-)
Mario Carneiro (Jun 28 2021 at 16:22):Pierre-Marie Pédrot said:
Huỳnh Trần Khanh that's the official propaganda of the party, CIC enjoys the same "theorem". The sad reality is that 1. by far most soundness bugs are due to implementation issues, not theoretical issues and 2. the theory actually implemented is not the one described in those papers.
The theory implemented by lean is a subset of the rules described in the paper. I was very careful to ensure this, because otherwise a soundness claim would be inappropriate as you say. I would very much like to extend the proof to cover Coq as well but there are a number of complicating factors and quite frankly I have no idea how to do it. (In particular, I don't know how to salvage unique typing, and the interaction of fixed and parametric universes seems... complicated; plus there are inductive and coinductive types and non-uniformly parametric inductives, all of which lean doesn't have to deal with.) As for undecidable type checking, that doesn't matter at all, because the soundness proof does not rely on strong normalization.
However (1) is certainly a concern. The main defense against this in lean is the external typecheckers, which can at least "dynamically" verify the correctness of proof deductions performed by the lean kernel. We run two external typecheckers on mathlib as part of CI, so that's a fairly good argument that there are not implementation bugs unless those bugs are shared by the external typecheckers (which is of course a possibility). But lean 3 has a spotless record in this regard: there has never been a soundness bug reported against the implementation.
Mario Carneiro (Jun 28 2021 at 16:32):Is it known that any soundness proof of Coq must depend on strong normalization? Or is the "obvious model" with types as sets sufficient? It is tricky to get an enumeration of all the features and ensure that they all respect the model. (As far as I know, the nearest equivalent to my paper in the Coq world is Coq Coq correct, but this is "just" a formalized typechecker, not a soundness proof, and it also doesn't cover some Coq features that any external typechecker would have to concern itself with to handle real world uses, like the module system
Paolo Giarrusso (Jun 29 2021 at 14:24):@Mario Carneiro modules could be left out of the kernel, in principle — they aren't in Coq, but it's not clear (EDIT: to me!) why. (see corrections below)
The "obvious model" isn't that obvious to work out for full Coq, but http://arxiv.org/abs/1710.03912 is the current last word on it.
Gaëtan Gilbert (Jun 29 2021 at 14:25):modules could be left out of the kernel, in principle
How would that work? Keep in mind we have functors
Paolo Giarrusso (Jun 29 2021 at 14:27):sorry, did I speak too quickly? Do you want soundness of uninstantiated functors? I _thought_ some of you complained that modules don't belong in the kernel? If not, forget it.
Paolo Giarrusso (Jun 29 2021 at 14:27):on the model, it's unclear that it doesn't rely on normalization... there's a nontrivial discussion, but IIUC that's true once you translate recursive functions to eliminators.
Pierre-Marie Pédrot (Jun 29 2021 at 14:59):First, the guard condition is probably the murkiest part of the Coq kernel.
Pierre-Marie Pédrot (Jun 29 2021 at 14:59):I conjecture that there are some recursive functions accepted by Coq that are not expressible via recursors.
Pierre-Marie Pédrot (Jun 29 2021 at 14:59):(we had a chat about that here some time ago)
Pierre-Marie Pédrot (Jun 29 2021 at 15:00):Second, fully instantiated functors are in theory expansible into plain terms, but the devil is in the detail.
Pierre-Marie Pédrot (Jun 29 2021 at 15:01):To prove this you'd need to take into account parameterized modules (i.e. functors) via some kind of logical relation, and then you have to think about the rules of the system.
Pierre-Marie Pédrot (Jun 29 2021 at 15:01):Mike Shulman is known to have abused the functor system and universe-polymorphic definitions to emulate Type_ω
Pierre-Marie Pédrot (Jun 29 2021 at 15:03):@Mario Carneiro unfortunately taking subset of a system is not going to preserve a lot of good properties of that system.
Pierre-Marie Pédrot (Jun 29 2021 at 15:03):It's trivial to break SR by a subset of the rules (and this is what happens in Lean)
Pierre-Marie Pédrot (Jun 29 2021 at 15:04):I personally find the claim that Lean is a single system on the verge of intellectual dishonesty. It's similar to claiming that ITT and ETT are the same thing. The "ideal" system is very nice but is undecidable, when the "real" system is ridden with technical issues.
Pierre-Marie Pédrot (Jun 29 2021 at 15:05):These two things can't be called "Lean" at the same time.
Pierre-Marie Pédrot (Jun 29 2021 at 15:07):(note that we're not merely talking about nice stuff to have, but what I consider foundational issues. The metacoq folks are heavily relying on properties such as SR to get anything done.)
Ali Caglayan (Jun 29 2021 at 15:09):Mike Shulman is known to have abused the functor system and universe-polymorphic definitions to emulate Type_ω
Do you have any more details on this? Are you referring to this blogpost?
Paolo Giarrusso (Jun 29 2021 at 15:12):To me, the clearest difference between @Pierre-Marie Pédrot and @Mario Carneiro 's position is philosophical — Pierre has conceptual objections to proving logical consistency using models into ZFC, and they have their importance; but if you accept that approach, subject reduction becomes much less important, so letting the algorithmic typechecker be incomplete becomes legitimate.
Paolo Giarrusso (Jun 29 2021 at 15:13):IIRC, that's also what happens with the SR violations in Coq with coinductives?
Pierre-Marie Pédrot (Jun 29 2021 at 16:34):@Ali Caglayan I think this is indeed the technique referred to in this post.
Mario Carneiro (Jun 29 2021 at 16:35):Pierre-Marie Pédrot said:
Mario Carneiro unfortunately taking subset of a system is not going to preserve a lot of good properties of that system.
You misunderstand. The lean system is a subset of the theory in the paper, not the other way around. In particular, this is why typechecking for the theory on paper is undecidable, while typechecking for the theory lean implements is decidable (obviously, since lean decides it by definition). It's true that adding additional rules to a system can break some properties (like decidability) or add new ones (like transitivity), but the one I care about is soundness, and if adding rules to a formal system results in a formal system that can't prove false, then the original system can't either.
Mario Carneiro (Jun 29 2021 at 16:37):Actually, looking again it seems you are interested primarily in SR. I was very upfront about these tradeoffs in my paper. Lean doesn't have all the nice things, it's true. I'm a lowly type theorist with no real power to change the foundations, only to document what they are
Mario Carneiro (Jun 29 2021 at 16:39):But if you ask me whether I should prefer a system that lacks SR or a system for which soundness is an open question, all other things being equal, the choice is obvious
Pierre-Marie Pédrot (Jun 29 2021 at 16:39):No, no, I understand that Lean the program is a subset of Ideal Lean.
Pierre-Marie Pédrot (Jun 29 2021 at 16:40):But if soundness is important, it's hardly the most important thing for a type theory, and this is probably where we disagree.
Pierre-Marie Pédrot (Jun 29 2021 at 16:41):Contrarily to many syntactic properties like SR and normalization, soundness is closed under subsystem, which is why it's fine to only implement a decidable Lean.
Mario Carneiro (Jun 29 2021 at 16:41):Pierre-Marie Pédrot said:
I personally find the claim that Lean is a single system on the verge of intellectual dishonesty. It's similar to claiming that ITT and ETT are the same thing. The "ideal" system is very nice but is undecidable, when the "real" system is ridden with technical issues.
Interesting that you mention this. My personal opinion is that lean should just embrace undecidability and go full ETT. Defeq causes so many problems in practice, I just want to be able to reason classically about equality and not worry about this maimed version of equality
Pierre-Marie Pédrot (Jun 29 2021 at 16:42):This has a lot of practical drawbacks though.
Pierre-Marie Pédrot (Jun 29 2021 at 16:42):This means you have to write your programs in a defensive stance.
Pierre-Marie Pédrot (Jun 29 2021 at 16:42):You'll never be sure than merely applying a conversion rule is not going to make the type-checker go crazy.
Pierre-Marie Pédrot (Jun 29 2021 at 16:43):Also, even extensional equality is not what you want in general.
Mario Carneiro (Jun 29 2021 at 16:43):Overuse of defeq is a code smell for me. Just write a lemma instead of applying a conversion rule
Mario Carneiro (Jun 29 2021 at 16:43):you never have to worry about the kernel going crazy if you just say what the proof is
Pierre-Marie Pédrot (Jun 29 2021 at 16:44):Well, yes, if you embrace undecidability the kernel can loop.
Mario Carneiro (Jun 29 2021 at 16:44):defeq can cause timeouts anyway
Pierre-Marie Pédrot (Jun 29 2021 at 16:44):you'll have to write explicit conversion steps everywhere and pray for the absence of coherence hell.
Pierre-Marie Pédrot (Jun 29 2021 at 16:45):this is true, and it's often an argument for "ETT is better in practice"
Mario Carneiro (Jun 29 2021 at 16:45):as long as the types stay simple you don't have to worry about coherence hell
Pierre-Marie Pédrot (Jun 29 2021 at 16:45):e.g. "What if the conversion asks for Ack(5,5) = blah"
Pierre-Marie Pédrot (Jun 29 2021 at 16:45):But what's the point of using dependent type theory then?
Mario Carneiro (Jun 29 2021 at 16:45):heh
Mario Carneiro (Jun 29 2021 at 16:45):the irony
Pierre-Marie Pédrot (Jun 29 2021 at 16:46):If I have to stick to HOL, I'd rather use Isabelle than Coq.
Mario Carneiro (Jun 29 2021 at 16:46):I usually say that dependent types make the impossible merely hellish
Mario Carneiro (Jun 29 2021 at 16:46):they should be used sparingly
Pierre-Marie Pédrot (Jun 29 2021 at 16:46):I think the mathcomp people are precisely the best supporters out there for dependent types
Mario Carneiro (Jun 29 2021 at 16:46):still better than not having them at all
Pierre-Marie Pédrot (Jun 29 2021 at 16:47):despite doing first order maths
Pierre-Marie Pédrot (Jun 29 2021 at 16:47):everything you can turn into a computation is a godbless
Mario Carneiro (Jun 29 2021 at 16:47):In lean/mathlib we take a tactic-first approach to that, in part because the lean kernel isn't as optimized for conversion-heavy calculations
Pierre-Marie Pédrot (Jun 29 2021 at 16:48):this is another interesting point btw
Pierre-Marie Pédrot (Jun 29 2021 at 16:48):I don't understand why this happens
Pierre-Marie Pédrot (Jun 29 2021 at 16:48):I'd be curious to learn why
Mario Carneiro (Jun 29 2021 at 16:48):plus lean has external typecheckers, are you going to ask them all to be super optimized for conversions too?
Pierre-Marie Pédrot (Jun 29 2021 at 16:48):why not?
Pierre-Marie Pédrot (Jun 29 2021 at 16:49):I mean, the mathcomp approach has proven that it was scalable
Mario Carneiro (Jun 29 2021 at 16:49):because that's a lot to ask for. It increases the TCB
Pierre-Marie Pédrot (Jun 29 2021 at 16:49):well, then you prove your checker.
Pierre-Marie Pédrot (Jun 29 2021 at 16:50):At some point the TCB argument becomes ironical when implementing a proof assistant.
Mario Carneiro (Jun 29 2021 at 16:50):hopefully in a simpler system...
Pierre-Marie Pédrot (Jun 29 2021 at 16:50):or not. I don't want to have to design another system and suffer writing FOL in it.
Mario Carneiro (Jun 29 2021 at 16:50):okay then it's still in the TCB
Pierre-Marie Pédrot (Jun 29 2021 at 16:50):not quite.
Pierre-Marie Pédrot (Jun 29 2021 at 16:51):If you go that way, Maxwell equations are part of the TCB.
Mario Carneiro (Jun 29 2021 at 16:51):of course they are
Pierre-Marie Pédrot (Jun 29 2021 at 16:51)::shrug:
Pierre-Marie Pédrot (Jun 29 2021 at 16:52):by proving a proof assistant in itself you still have enhanced the trustability of the code by several orders of magnitude
Pierre-Marie Pédrot (Jun 29 2021 at 16:53):and in any case at some point you have to bite the bullet of Gödel's incompleteness theorem
Mario Carneiro (Jun 29 2021 at 16:53):I don't disagree with you at all, that's the topic of my upcoming PhD thesis. But I would also want a self verified system to be as philosophically parsimonious as it can reasonably be
Paolo Giarrusso (Jun 29 2021 at 22:06):Pierre-Marie Pédrot said:
But what's the point of using dependent type theory then?
universal algebra? :grinning_face_with_smiling_eyes:
Jonathan Sterling (Jun 29 2021 at 22:25):IMO "TCB" is a myth invented to write introductions to general-audience papers on theorem proving... It has so little pertinence to the everyday use of proof assistants as to be laughable.
Pierre-Marie Pédrot (Jun 30 2021 at 10:16):My thought capacity has been permanently maimed by the Internet, and I cannot help thinking that the "will you fight, or will you perish like a dog meme" is curiously fitting this conversation. Should we embrace meta-self-objectification?
Matthieu Sozeau (Jul 07 2021 at 10:14):Interesting discussion :-) Probably irrelevant to most first-time users though! I think TCB has quite some importance in the case of Coq, where the kernel is quite big and complex and where we repeatedly found bugs. Admittedly, we found nothing unfixable or having a huge impact on users (to date), except maybe all the subtle template-polymorphism bugs that led us to restrict the feature. Compared to the external checker of Lean or an LCF HOL-like kernel, the Coq kernel is qualitatively different: it really does not read like a spec.
Matthieu Sozeau (Jul 07 2021 at 10:16):The other point where TCB has importance is when we talk to certification agencies. They need some slightly tangible measure of "trust"
Meven Lennon-Bertrand (Jul 07 2021 at 10:19):But hopefully we won’t have to trust the Coq kernel anymore, only MetaCoq! And this will definitely be for the best. Especially because the need to keep a somewhat reasonable kernel to trust forces us to rely on a heavy elaboration layer, when some stuff could be kept as is rather than elaborated if we had a larger kernel.
Matthieu Sozeau (Jul 07 2021 at 10:32):Mario Carneiro said:
Is it known that any soundness proof of Coq must depend on strong normalization? Or is the "obvious model" with types as sets sufficient? It is tricky to get an enumeration of all the features and ensure that they all respect the model. (As far as I know, the nearest equivalent to my paper in the Coq world is Coq Coq correct, but this is "just" a formalized typechecker, not a soundness proof, and it also doesn't cover some Coq features that any external typechecker would have to concern itself with to handle real world uses, like the module system
That's a good question. The gap can be found as the difference between Coq in Coq's formalism (which has a ZF relative soundness proof) and MetaCoq's PCUIC Calculus. In short, universes are easy, parametric inductive, families and even non-uniform parameters are handled in the model already. Mutual inductives are easy, but nested ones are not handled AFAIK (and we suspect with Pierre-Marie that it says something "interesting"). Coq in Coq is also using a sized-types discipline that is slightly different although not entirely unrelated to guard checking. Bridging this gap will probably require a PhD. And the module system is not considered (we could handle functor-free modules quite easily though, I suppose, but maybe a reworking that elaborates modules to more expressive record types would be better and factorize the problem), nor "fast" bytecode and native-compute conversion algorithms, nor template-polymorphism.
Jonathan Sterling (Jul 07 2021 at 12:39):Matthieu Sozeau said:
Mario Carneiro said:
Is it known that any soundness proof of Coq must depend on strong normalization? Or is the "obvious model" with types as sets sufficient? It is tricky to get an enumeration of all the features and ensure that they all respect the model. (As far as I know, the nearest equivalent to my paper in the Coq world is Coq Coq correct, but this is "just" a formalized typechecker, not a soundness proof, and it also doesn't cover some Coq features that any external typechecker would have to concern itself with to handle real world uses, like the module system
That's a good question. The gap can be found as the difference between Coq in Coq's formalism (which has a ZF relative soundness proof) and MetaCoq's PCUIC Calculus. In short, universes are easy, parametric inductive, families and even non-uniform parameters are handled in the model already. Mutual inductives are easy, but nested ones are not handled AFAIK (and we suspect with Pierre-Marie that it says something "interesting"). Coq in Coq is also using a sized-types discipline that is slightly different although not entirely unrelated to guard checking. Bridging this gap will probably require a PhD. And the module system is not considered (we could handle functor-free modules quite easily though, I suppose, but maybe a reworking that elaborates modules to more expressive record types would be better and factorize the problem), nor "fast" bytecode and native-compute conversion algorithms, nor template-polymorphism.
Hi @Matthieu Sozeau, I hope you are well! Maybe this is a chance for me to ask a question. Coq-as-implemented has a number of eta laws (for instance, eta laws for function types and for some record types). Are both of these accounted for in the metacoq formalization? I had a look at MetaCoq.Checker.Typing and I couldn't find it.
Kenji Maillard (Jul 07 2021 at 13:13):@Meven Lennon-Bertrand this one is for you I think
Matthieu Sozeau (Jul 07 2021 at 13:31):Hi Jonathan, I'm fine! Indeed, they are not part of it today, but we're working on it with @Meven Lennon-Bertrand and @nicolas tabareau We think we can get eta for function types, non-empty record types and SProp's strict equality as well, even in this purely untyped setting.
Jonathan Sterling (Jul 07 2021 at 13:33):Great to hear that! This has been one of my concerns about the MetaCoq direction, since I have felt that Coq aspires to implement a style of type theory for which these untyped techniques tend to be not so well-adapted. (The fact that there seems to be little hope for the record type without any fields is indicative of this.) But I would be very happy if you get the non-empty records working! Thanks :)
Matthieu Sozeau (Jul 07 2021 at 13:38):I also believe that to go beyond that, one needs to put some typing information in the syntax, or rely on retyping during conversion (as Agda does, AFAIK)
Matthieu Sozeau (Jul 07 2021 at 13:41):In another direction we think we might be able to show rather straightforwardly that the theory with judgmental equality rules is equivalent to the current untyped version, that would be reassuring w.r.t. all the nice work done on categorical models ;-)
Meven Lennon-Bertrand (Jul 07 2021 at 14:18):@Jonathan Sterling The interesting thing is that although the theories as usually described on paper are quite different, the actual algorithms as implemented respectively in Agda and Coq are much more similar, as far as I understood. Terms are wh-reduced then compared, and the only difference for η on functions is the way it is fired at that stage: Agda (and NbE as well, I guess) use it systematically when comparing terms of function types, while Coq only fires it when comparing a neutral with a λ-abstraction, while in case there are two λ against each other it directly uses congruence (which is the same as η-expansion followed by β-reduction), and otherwise compares the neutrals directly without η-expanding them.
So my hope is that one could prove the undirected systems equivalent to algorithmic/bidirectional ones, and then prove the equivalence between the algorithmic systems. But indeed we are hitting real hard into the pains of rewriting.
Cody Roux (Jul 07 2021 at 16:15):Dang, I got to this thread late... I'd sure love a thread where we sketch the proofs of these things!
Jonathan Sterling (Jul 07 2021 at 16:21):Matthieu Sozeau said:
In another direction we think we might be able to show rather straightforwardly that the theory with judgmental equality rules is equivalent to the current untyped version, that would be reassuring w.r.t. all the nice work done on categorical models ;-)
Yes, to me the second idea sounds like a good one --- then (in principle) one can use a better-adapted method such as nbe (or the mathematical versions thereof) to establish the metatheory of Coq. It seems like if one wants Coq to have such laws, then it may be a mistake to formulate Coq's metatheory in terms of rewriting. Furthermore, it would be nice to add the eta law for the unit type, which is not problematic in the setting of nbe.
Matthieu Sozeau (Jul 08 2021 at 07:11):The thing is, we are kind of starting from the implementation here, so we have to go though the rewriting metatheory at some point, ensuring confluence/transitivity and show that it models a congruence relation which is otherwise part of the judgmental equality specification. But yeah in the future we might just get rid of untyped equality and switch to an nbe algorithm, if we can get that to scale. One thing that's worrying with the eta rules for e.g. records is that blind expansion (nbe style) could bring terrible performance issues in libraries like math-comp where records are everywhere in unification and conversion problems.
Pierre-Marie Pédrot (Jul 08 2021 at 10:14):From a performance point of view, unfolding of δ-δ conversion problems is critical. I think that if one were to use NbE for that, even without considering records, there would be an unbearable efficiency hit, because NbE internalizes δ rules so much that they are transparent. It's fine to use NbE for the spec though.
Jonathan Sterling (Jul 08 2021 at 15:18):Matthieu Sozeau said:
The thing is, we are kind of starting from the implementation here, so we have to go though the rewriting metatheory at some point, ensuring confluence/transitivity and show that it models a congruence relation which is otherwise part of the judgmental equality specification. But yeah in the future we might just get rid of untyped equality and switch to an nbe algorithm, if we can get that to scale. One thing that's worrying with the eta rules for e.g. records is that blind expansion (nbe style) could bring terrible performance issues in libraries like math-comp where records are everywhere in unification and conversion problems.
Indeed... It is one thing to answer these questions in theory, but it is quite another to try and get those answers to scale to something like Coq. The issue with records is very true --- for instance, Agda has this no-eta flag that you can set on records which some users have needed in order to maintain acceptable performance for certain use-cases.
Jonathan Sterling (Jul 08 2021 at 15:21):Pierre-Marie Pédrot said:
From a performance point of view, unfolding of δ-δ conversion problems is critical. I think that if one were to use NbE for that, even without considering records, there would be an unbearable efficiency hit, because NbE internalizes δ rules so much that they are transparent. It's fine to use NbE for the spec though.
Oh and btw, I am not proposing that you should use an nbe algorithm --- there are many aspects of nbe that are way too naive for a serious implementation. But there are aspects of the technique that could likely be applied, and it seems like "type directed conversion" (with some optimizations) is a good direction to go, if Coq does indeed want to have all the extensionality laws that it currently implements.
And yeah, I also want to distinguish between the implementation and the spec. There is always a greater distance between these things than people think, and to me that is OK.
Meven Lennon-Bertrand (Jul 08 2021 at 15:41):Jonathan Sterling said:
Oh and btw, I am not proposing that you should use an nbe algorithm --- there are many aspects of nbe that are way too naive for a serious implementation. But there are aspects of the technique that could likely be applied, and it seems like "type directed conversion" (with some optimizations) is a good direction to go, if Coq does indeed want to have all the extensionality laws that it currently implements.
Coq already implements some cheap bits of type directed conversion though. For instance the implementation of SProp using relevance marks is basically a way to transport a small bit of information ("is this term in a type in SProp?") that is enough to trigger extensionality rules without carrying the whole typing information.
Jonathan Sterling (Jul 08 2021 at 19:38):Meven Lennon-Bertrand said:
Jonathan Sterling said:
Oh and btw, I am not proposing that you should use an nbe algorithm --- there are many aspects of nbe that are way too naive for a serious implementation. But there are aspects of the technique that could likely be applied, and it seems like "type directed conversion" (with some optimizations) is a good direction to go, if Coq does indeed want to have all the extensionality laws that it currently implements.
Coq already implements some cheap bits of type directed conversion though. For instance the implementation of SProp using relevance marks is basically a way to transport a small bit of information ("is this term in a type in SProp?") that is enough to trigger extensionality rules without carrying the whole typing information.
Indeed, as it must!
Cody Roux (Jul 09 2021 at 18:17):Pierre-Marie Pédrot said:
From a performance point of view, unfolding of δ-δ conversion problems is critical. I think that if one were to use NbE for that, even without considering records, there would be an unbearable efficiency hit, because NbE internalizes δ rules so much that they are transparent. It's fine to use NbE for the spec though.
Isn't there a way to make NbE as sophisticated as the "reduction based" algorithm though? Basically reify an ident as either a "neutral" or a "value" depending on a similar heuristic as currently. This requires adding a new class of neutrals though.
Maybe @Jonathan Sterling has some insight.
Paolo Giarrusso (Jul 10 2021 at 16:56):@Cody Roux
Would you count sth like https://github.com/inc-lc/ilc-scala/blob/master/src/main/scala/ilc/feature/let/BetaReduction.scala#L175-L181 as an example? That (claims to) handle shrinking reductions, confirming the idea's pretty flexible, as long as you have one notion of normal form and at least for something like "defunctionalized" NbE, where you still use a custom evaluator, as used by Andreas Abel and others (including http://www.jonmsterling.com/pdfs/modal-mltt.pdf with @Jonathan Sterling and others). You can probably partially evaluate that to improve the constant factors (the extra checks would happen in the first stage), but I'm not sure how well it'd fit with native compute.
Paolo Giarrusso (Jul 10 2021 at 17:02):However, that's for normalization, while Coq needs conversion checking, and I think "normalize and compare" is far from what happens... the experience (when abusing Coq) is that it tries to not unfold your definition, heuristically, and backtracks to unfolding if the first attempt fails.
Gaëtan Gilbert (Jul 10 2021 at 17:04):with VM and native normalize and compare is fairly accurate AFAIK
Paolo Giarrusso (Jul 10 2021 at 17:04):I say "abusing Coq" because this is visible if you abuse Coq by chain enough unsealed definitions (as I did in my first Iris project): there type errors show up as "apply seems to loop forever instead of terminating instantly".
Paolo Giarrusso (Jul 10 2021 at 17:05):@Gaëtan Gilbert right, but I suspect that "NbE internalizes δ rules so much that they are transparent" hints at this kind of seeming backtracking?
Gaëtan Gilbert (Jul 10 2021 at 17:07):deltas are transparent in vmnative
Paolo Giarrusso (Jul 10 2021 at 17:10):right, because that's using (non-type-directed?) NbE (strong reduction's another name for it), so that can't be the @Pierre-Marie Pédrot's point, can it?
Gaëtan Gilbert (Jul 10 2021 at 17:12):most conversions are checked with lazy, not vmnative
Cody Roux (Jul 12 2021 at 13:00):Yes, indeed the heuristics for reduction might be distinct from the heuristics for conversion checking, though I feel like that definitely doesn't preclude using some flavor of NbE. @Paolo Giarrusso that Scala code is really cool!
Last updated: Oct 03 2023 at 04:02 UTC