Replying to
Lean. One kernel bug. In the darkest type theory. All external checkers affected. Learn why this matters in the AI age.
Remote
Meven Lennon-Bertrand
@mevenlennonbertrand@lipn.info
mastodon 4.7.2Post-doc at INRIA/IRIF/Université Paris Cité.
I mostly try to convince proof assistants that they are doing reasonable things. Sometimes this involves studying type theory. Sometimes this means understanding what our implementations do. All in all, it's not too bad.
Profile banner (from the Leonard comic by Turk & de Groot):
- I wanted to serve science because it it my joy and instead of that, what am I doing?...
- Yes, what is he doing?
- I guess he's complaining!
557 Followers
153 Following
50 Posts
Joined April 22, 2024
web page:
proof assistants stack exchange:
pronouns:
he/they
Replying to
I'm not very good at this, am I?
Replying to
@jonmsterling@mathstodon.xyz Yeah, had this happened 6 months ago my application case would have been much easier to make too 🙃
Replying to
@TaliaRinger@mathstodon.xyz I think type theorists would consider this as rather applied type theory :p But fully agreed!
On the positive side (and to toot my own horn a bit) we have not been idle: https://metarocq.github.io/ is the most mature project in the area, but https://github.com/digama0/lean4lean and https://github.com/jespercockx/agda-core/ are also busy, and there's a lot of more fundamental research happening as well to prepare for these project's next steps. The age of verified kernels is coming!
Replying to
@jonmsterling@mathstodon.xyz There was an absolute horror story at the Types business meeting: an email by a very generous Swedish foundation accepting to sponsor the conference was lost in Microsoft quarantine for months…
RE: https://mastoxiv.page/@arXiv_csLO_bot/116169963926058915
Lately I've embarked on a fun side quest in proof theory. Where I managed to still bump into bidirectional typing! (To an old dog everything looks like a nail, that's the saying right?)
I learned bidirectionalism is very much related to the subformula property, a proof theory idea that had always seemed mysterious to me. Now I understand why proof theorists rave about cut elimination and the subformula property, which is the same as why bidirectionalism is so useful for proofs: information flow! Also the coincidence between normal forms and terms having good bidirectional typing seems less miraculous: it's essentially the same thing as cut-free proofs having the subformula property.
So anyway, interpolation is a cute property, but I learned a surprising amount about type theory while looking at it! Hope you will too.
Another day, another rant about injectivity: https://proofassistants.stackexchange.com/questions/6533/why-does-lean4-use-intensional-type-theory-when-its-definitional-equality-is-und
Am I an old broken record already?
Replying to
@mattblaze@federate.social @0xabad1dea@infosec.exchange I think it's practically ok, we have good human measures in place to avoid such bugs having serious consequences. Of course, on the long run this is a strong motivation to apply serious formal methods to proof assistant kernels, ideally towards full verification!
Replying to
@jesper@agda.club Congrats!!
@arretsurimages@mamot.fr trahi par ses liens... Pour un média qui analyse la déliquescence du paysage informationnel et se rit des faux-pas des autres, c'est assez ironique 😬
Replying to
@mio@shrimp.mio19.uk Many of us are!
Replying to
@rntz@recurse.social I think the "not" I mean here is a very innocuous operation (pattern-matching on a datatype), which is not the nasty negation you likely have in mind. In domains the logic programmer's "not" would rather correspond to the operation on the Sierpinsky space \( 1_{\bot} := \{\bot, \star\}\) (with \(\bot < \star\)) , which exchanges \(\bot\) and \(\star\), and is also not valid since it's not monotone.
But I don't see any fundamental difference between por and pand, both evaluate their two branches in parallel and shortcut evaluation whenever one of them returns. What values are returned is not very relevant, what is is the parallel nature of evaluation.
Replying to
@yforster@types.pl And I guess that would be @ramana@masto.xrchz.net ? But that's fair, I'd like to know more about the original context for the bug finding (and correct the story accordingly) :)
Replying to
@rntz@recurse.social Don't we have pand x y = (not (por (not x) (not y))?
In general, parallel or is all you need for the "standard" denotational semantics of PCF in domains to be fully abstract, so in a sense it gives you "all the parallelism you need", and other similar constructs like your pand should be definable from it.
Replying to
@julesh@mathstodon.xyz @lisyarus@mastodon.gamedev.place This is a baby version of Stone duality, ie the fact that Set^op is equivalent to the category of complete atomic boolean algebras : in one direction, you map a set to its powerset, which is a CABA ; in the other direction, you map a CABA to its set of atoms (elements x st y < x implies y = ⊥). Indeed, the atoms in a powerset are exactly the singletons, and a set is isomorphic to the set of its singleton. (The good thing is that this is nicely structural, and does not need to play set-theoretic trickery with unions or some such.)
Replying to
@mc@mathstodon.xyz I'm a bit torn on this. On the one hand I agree with others in this thread that, even in a formalization-oriented venue, I expect a paper to bring something new, either on the formalization side (a new approach, technique, tooling, etc) or the topic side (a new proof, new result...). But on the other hand, I believe that contributing to the body of formalised mathematics/CS, in the form of reusable library code is also valuable, even if it brings little new insight. I don't know how we should support such work, papers feel like the wrong currency, but sadly they're the academic credit...
Another day in "having a reliable aka complete kernel is pretty nice", from @BeLazy@types.pl: fixing incompleteness issues with η for unit fixes open issues with pattern-matching compilation!? (PR: https://github.com/leanprover/lean4/pull/12636)
Did you know that Rocq has very good looking badges to include in your next paper/repo/etc? https://github.com/rocq-prover/rocq-prover.org/tree/9529d3ee4f4c86c5cc73650f2c07d06fa458762c/rocq-id/badges
Replying to
@rntz@recurse.social Tooting my own horn (although I barely contributed to its great material), but an elementary reference on the domain semantics of PCF is Cambridge's denotational semantics course: https://www.cl.cam.ac.uk/teaching/2526/DenotSem/ It only touches quickly upon por, but contains references to more advanced material.
This was a very well-understood topic in the 90s, so you have quite a few good courses/textbooks on the topic (eg Gunter's).
Replying to
@raito@nixos.paris All that I publicly found on this is elsethread!
Replying to
@chrisamaphone @pigworker There are some bits of this formalised in Agda, as reported in https://arxiv.org/abs/2409.02603 (iirc the paper focuses on the fixed point part, but the formalisation does more)
Replying to
@koronkebitch 🫂 You're not alone! My main motivation when doing this job is to create something for others: a tool, theorem, a library, a lecture, an idea... I have fun solving the puzzles too and am addicted to the proof assistant rush, but the real deal is when someone comes and says "hey, that's neat, can I use it?". Many of us are like this, doing what they do for the humans rather than against them. Maybe right now they're a bit quiet in the midst of all the noise, but they won't go away, I'm sure of it.
@edwinb@types.pl @gallais@mamot.fr I want to cite the fact that Idris 2 has `Type : Type`. Is there anything more authoritative than the note in the FAQ saying “Idris 2 currently implements Type : Type. Don’t worry, this will not be the case forever!”? (Also, just to be sure: is this note still up to date?)
Replying to
@jonmsterling @jeanas @jpoiret @carloangiuli The core idea is perhaps unsurprising: if you only quote close normal forms, everything is fine wrt to congruence. Still, this gives a very direct construction for "relevant" CT (the one with a Sigma type).
Replying to
@ionchy@types.pl @jesper@agda.club Afaiu there's huge fights over those CO2/token numbers because depending how you take training cost into account the results vary wildly?
Replying to
@rntz@recurse.social (Technically I'm a bit wrong: full abstraction is weaker than definability of all elements of the model, and I don't remember whether this stronger property also holds for the domain model of PCF+por)
Replying to
@MartinEscardo That's just what I (jokingly) meant in the next sentence ;)
So yes to some extent it is, since this is very much me trying to make sense of proof theory I am re-casting it with my own words. But somehow what I wanted to put forward is that it brought a new (to me) light on something (bidirectional typing) I already understood, by looking at it in a different context. It's probably a bit pretentious a claim at this stage, but I feel this is a tentative new entry in the Curry-Howard correspondence, which, as we know, is a nice way to understand things we think we know.
Replying to
Replying to
@chrisamaphone@hci.social That's the high life
Replying to
@pigworker @jonmsterling I really feel like we are missing a hammer (or rather, a fine tool) to give us what confluence gives us re:patterns and the like, without having to worry about normalisation.
Replying to
@constantine@types.pl Iirc @HarrisonGrodin@mathstodon.xyz was trying to do something like that in January, tagging him in case it's of interest!
Replying to
@markusde@mathstodon.xyz Isn't the point that having a proof on the Rocq side + a proof that the statement translated from Lean is equivalent to the Rocq one makes it reasonable to not translate the whole proof? I find it not quite fully satisfying, but the approach sounds honestly very reasonable to me.
Replying to
@koronkebitch@types.pl Wow, so cool!
Did you know: the only image of Michel Rolle available on the internet is, in fact, a low resolution picture of Leibnitz.
(Rolle is known by every French math student because the standard construction of analysis here goes through the theorem named after him, is it one of those cases where we're the only ones doing it this way or is the guy actually famous?)
Replying to
@ohad@mathstodon.xyz @mc@mathstodon.xyz I never said one should bar unformalized ideas!? (And think this would be a terrible idea, too)
Replying to
@matematiflo@mathstodon.xyz @de_Jong_Tom@mathstodon.xyz Looking forward to it!
Replying to
@jonmsterling@mathstodon.xyz Can you say a little bit more about what you have in mind with your first point? I'm definitely curious/interested!
Replying to
@jonmsterling @jpoiret @carloangiuli Whoop my bad I got mixed up. Indeed the "reasonable' version you need for synthetic computability is compatible. A quoting operation properly integrated in the type theory is a pretty funny thing, and that one contradicts funext, but it's arguably even more niche than CT.
Replying to
@pigworker Follow up on @jonmsterling's question on η: have you given any thoughts as to what happens to *other* equations we definitely want to have, eg ν rules, or anything that goes beyond mere arithmetic, really?
Replying to
@danielgratzer @de_Jong_Tom Thanks a lot for trying to make it work!
Replying to
@MartinEscardo@mathstodon.xyz Re: trusting C code, I heard horror stories about compilers for aeronautics, where one of the criteria for acceptance is that the "compiler" is very transparent and that the assembly code is auditable on its own. Apparently, getting these sort of people to accept an optimising compiler, even CompCert, was a hard battle… (But it was won!)
Replying to
@chrisamaphone New addiction just dropped 👀
Replying to
@chrisamaphone @wilbowma One should definitely be able to say that copyright is not a great framework to support a society where creative work can be rewarded but at the same time that the way the AI industry is organised is extremely harmful. (But I guess in your words @willbowma this is part of the power argument? Although I don't see how you can argue about copyright without arguing about power: copyright is in principle a tool to give power to creators...)
Replying to
@ncf Argh! Thanks for the catch, the reference should be to https://dl.acm.org/doi/10.1145/3354166.3354168 Looks like not being able to \textcite made us fail to realize we were citing the wrong Abel2019… We'll fix it in the next version
Replying to
@jonmsterling@mathstodon.xyz I think I have a vague idea of what you have in mind. I guess this is related to the LCF-like approach you mentioned for Pterodactyl a while ago? And I guess the big difference with Andromeda 2 is, as you say, that when the TT does not suck you have access to much more meta-theorems/operations via the interface?
I've been thinking about somewhat similar things (although probably not quite) recently, along the lines of "verifying an implementation when you are given only a GAT and its metatheory". This case too should not be extremely hard, but nonetheless interesting.
In any case, happy to chat!
Replying to
@markusde@mathstodon.xyz Have you seen what can be done with this nowadays https://theoremlabs.com/blog/lf-lean/ ?
Replying to
@jonmsterling @jpoiret @carloangiuli Church Thesis, for synthetic computability theory. This is by now a well-installed topic, if maybe a bit niche, and imho a much more elegant way to formalise computability theory that all the other alternatives.
Now I'm not saying that you should abandon funext in your standard mathematical life just to stay compatible with CT. But there is at least one non-hypothetical application for negating it.
Replying to
@markusde@mathstodon.xyz I guess it says that :
- the definitions give you objects which once roundtripped are isomorphic to the original ones ; not the best specification, but rather solid (it rules out everything being unit or something, and is especially fine if you also translate the various operations/basic proofs which encode that they behave the way one expects)
- the lemmas you admit on the Lean side are logically equivalent (up to Lean -> Rocq translation) to ones which are proven, which to me makes them very reasonable to assume
Of course that brings the Lean -> Rocq translation to the TCB, as well as Rocq, but I still feel this is ok?
And I don't see how the liking with other Lean code changes anything, you can treat the translated code as some sort of opaque module with a bunch of definitions and proofs and use that opaquely, just as you would any other Lean module? Except in this one the proofs are not there, they're on the Rocq side