Stream: Miscellaneous

Topic: Discussing Lean's foundations


view this post on Zulip Michael Soegtrop (Jun 12 2020 at 12:51):

@Bas: can you elaborate a bit on the Lean vs Coq ranking? it is very close but still I would be interested to learn what reasoning is behind that order.

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 12:54):

Totally notwithstanding the fact that Lean is written in C++ and just that makes it more suspicious...

view this post on Zulip Karl Palmskog (Jun 12 2020 at 12:56):

Bas can confirm, but in my mind Gaëtan's experiment showed that Coq's foundations are more flexible than Lean's, and template polymorphism bugs may not help either... so non-type-theorists may have to implicitly trust more stuff.

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 12:58):

As a type theorist, I personally consider the foundations of Lean to be broken by default...

view this post on Zulip Pierre-Marie Pédrot (Jun 12 2020 at 12:58):

At least in Coq you have to opt-in to wreak havoc with the type system

view this post on Zulip Paolo Giarrusso (Jun 12 2020 at 12:59):

Lean has multiple independent checkers, including one in Haskell, so I recommend ignoring the C++ part.

view this post on Zulip Paolo Giarrusso (Jun 12 2020 at 13:03):

and if you don't buy Lean foundations or consistency proofs, you're also questioning Mizar (that uses a set theory stronger than ZFC) and probably many of the other systems (does even HOL survive?)

view this post on Zulip Théo Zimmermann (Jun 12 2020 at 13:11):

Pierre-Marie has repeatedly expressed specific concerns about some properties that Lean developers do not even try to have, but I believe that soundness is not one of them.

view this post on Zulip Enrico Tassi (Jun 12 2020 at 13:29):

I think they don't have subject reduction which is a property that is typically used to prove soundness.

view this post on Zulip Enrico Tassi (Jun 12 2020 at 13:41):

Karl Palmskog said:

Bas can confirm, but in my mind Gaëtan's experiment showed that Coq's foundations are more flexible than Lean's, and template polymorphism bugs may not help either... so non-type-theorists may have to implicitly trust more stuff.

This kind of argument is, in my opinion, quite fallacious. If you take the HOL family for example, the kernel does not even understand "nat := S nat | Z". Of course the kernel is smaller, but you also have to trust some other code that does the encoding. IMO the fact that you can encode A in B, does not mean that B is more trustworthy, nor less. It just makes it harder to define where the TCB ends. Especially given that the encodings are often "extra logical" hence they don't even help relating the power of the logics (for example the encoding HOL in Coq needs axioms).

I guess making people conscious that there is no miracle, all tools can be buggy, and some a more rigorous that others, is important. But ranking tools is too hard to me.

Little anegdote: the type checker of Elpi has been incredibly useful in the development of HB. I know for sure (since I wrote it) that it is a hack, unsound and incomplete (I'm so ashamed that I'll rewrite it, at some point...). Morale: even the verification you do with a broken tool can be useful ;-)

view this post on Zulip Michael Soegtrop (Jun 12 2020 at 13:56):

Pierre-Marie has repeatedly expressed specific concerns about some properties that Lean developers do not even try to have, but I believe that soundness is not one of them.

An interesting formulation ;-)

I wonder how system like Dedukti change this trust landscape. Since an automated translation from one logic to another would not be trustworthy, one would have to manually check the top level specs in the translated form. I can imagine that this is simpler if the source logic is more expressive because the specifications would allow a more natural encoding of specifications.

view this post on Zulip Paolo Giarrusso (Jun 13 2020 at 12:55):

I know issues about Lean have been raised, but I’m unconvinced that impredicative type theory has a better story, and I’m unsure if “impredicative Prop” is predicative enough for this discussion.

view this post on Zulip Paolo Giarrusso (Jun 13 2020 at 12:57):

AFAIK, outside of predicative type theory, the normal way to prove soundness and consistency relies on a stronger metatheory — which is what happens for Lean and non-type theoretic systems — including HOL, I expect?
Now, impredicative type theories (up to Coq with impredicative Set) does that too — consistency relies on strong normalization which relies on an impredicative metatheory!

view this post on Zulip Paolo Giarrusso (Jun 13 2020 at 13:02):

The only arguably-better story which I’ve seen is predicative type theory with Martin-Löf’s meaning explanation. You might be able to model proof-irrelevant impredicative Prop with a boolean model in a predicative metatheory — but does that scale to full Coq with cumulativity etc.? Otherwise, I’m not sure why I should trust Coq more than Lean.

view this post on Zulip Bas Spitters (Jun 13 2020 at 13:04):

As we all know, due to @Gaëtan Gilbert , coq is a great type checker for lean.

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:15):

@Paolo G. Giarrusso my personal problem with Lean is not predicativity vs. impredicativity. I am fairly confident about impredicativity actually, and never quite understood why the Swedish school of constructive mathematics were that traumatized by it. Heck, I actually have no problem with ZFC + whatever big cardinal assumption as far as soundness goes.

No, my grudge against Lean is that you can't really trust the computational content of the proofs because of the lack of decidable type-checking and the subsequent loss of subject reduction. You pick a term, you compute with it, and it might happen that the result doesn't even type-check.

view this post on Zulip Enrico Tassi (Jun 13 2020 at 13:18):

Pierre-Marie Pédrot said:

Paolo G. Giarrusso my personal problem with Lean is not predicativity vs. impredicativity. I am fairly confident about impredicativity actually, and never quite understood why the Swedish school of constructive mathematics were that traumatized by it.

Because at some point they proposed an impredicative system that was broken ;-)

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:18):

Fair enough, but then this is entering a Freudian territory.

view this post on Zulip Enrico Tassi (Jun 13 2020 at 13:18):

Indeed

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:19):

LISP got static binding wrong, that's not a reason to reject higher-order functions on those grounds...

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:20):

I think it's still an open problem whether System F can be proved SN predicatively.

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:20):

As far as my personal beliefs go, I have no doubt that System F is SN...

view this post on Zulip Enrico Tassi (Jun 13 2020 at 13:20):

I agree, I was mostly joking

view this post on Zulip Kenji Maillard (Jun 13 2020 at 13:20):

@Pierre-Marie Pédrot If you use the "idealized" non-decidable conversion rule that lean is theoretically using, won't you recover subject reduction ? Or is there another obstruction beside the impossibility in general to re-typecheck an evaluated term ?

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:21):

@Kenji Maillard yes, you can pick your poison: non decidable type-checking or no SR.

view this post on Zulip Kenji Maillard (Jun 13 2020 at 13:21):

Well, I'm usually fine with having a theoretical SR

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:21):

but this claim that there is the idealized system and the actual implementation is nonsense to me

view this post on Zulip Kenji Maillard (Jun 13 2020 at 13:22):

I mean I won't try to retypecheck an evaluated term because it will often be impractical, no ?

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:22):

@Kenji Maillard then you also break computation in some sense

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:22):

it's not necessarily reduction, it pervades into conversion actually

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:23):

this brings in the same kind of issues that ETT has

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:23):

i.e. you can apply computational equations to the term but there is no reason that they are equi-typable

view this post on Zulip Kenji Maillard (Jun 13 2020 at 13:24):

hm, you mean if ΓAok\Gamma \vdash A \,ok and ABA \equiv B you don't necessarily have ΓBok\Gamma \vdash B ok ?

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:24):

so in practice you made the whole computational content of the theory highly dubious

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:24):

@Kenji Maillard yep

view this post on Zulip Enrico Tassi (Jun 13 2020 at 13:25):

It wold be worse if you had A ok, A = B, B ko ;-)

view this post on Zulip Enrico Tassi (Jun 13 2020 at 13:25):

as in PHP

view this post on Zulip Kenji Maillard (Jun 13 2020 at 13:27):

I'm still a bit puzzled: Isn't it just that the typechecking algoritm and the conversion procedure are not complete with respect to their specs ?

view this post on Zulip Paolo Giarrusso (Jun 13 2020 at 13:27):

Yeah, won’t you get B okay using the “idealized system”? (I don’t care for decidable complete typechecking either)

view this post on Zulip Enrico Tassi (Jun 13 2020 at 13:34):

Kenji Maillard said:

I'm still a bit puzzled: Isn't it just that the typechecking algoritm and the conversion procedure are not complete with respect to their specs ?

I guess that is more like "they can't be"

view this post on Zulip Kenji Maillard (Jun 13 2020 at 13:34):

Well I do think that being complete is an important property (also in practice): when your program does not typecheck you know that the problem is either in the program itself or it's a bug of the typechecker (possibly a performance bug)

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:38):

Completeness defines the type theory

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:38):

I really don't understand the claim that Lean as implemented is an approximation of the idealized theory.

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:39):

It's just not true, they are two different theories.

view this post on Zulip Kenji Maillard (Jun 13 2020 at 13:44):

I guess that is more like "they can't be"

Fair enough :)

Completeness defines the type theory

Do you mean that there are cases where Γidealt:A\Gamma \vdash_{ideal} t : A holds but the lean typechecker will say Γ̸leant:A\Gamma \not\vdash_{lean} t : A instead of saying that it is unable to answer in finite time ?

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:44):

Have you heard about the halting problem?

view this post on Zulip Kenji Maillard (Jun 13 2020 at 13:45):

I think someone told me about these kind of horror stories when I was a kid ^^

view this post on Zulip Kenji Maillard (Jun 13 2020 at 13:52):

but I still don't see how it applies here (sorry to be so slow; or maybe just ignorant).
If you have a program that you try to typecheck for an intrisically semi-decidable type system you could have 3 kinds of outputs:

(I'm assuming that you want to write a total typechecker of course)

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:55):

I don't understand how having a tri-valued function helps...

view this post on Zulip Kenji Maillard (Jun 13 2020 at 13:58):

I'm trying to understand what you mean by "completeness defines the type theory": this tri-valued function does not define any type theory but it would still validate the spec of the undecidable type theory.

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:59):

I don't understand how you define the "practical" type theory

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 13:59):

you can always semi-decide that something is in the idealized type theory, I agree

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 14:00):

but the stuff that says I don't know you never really know

view this post on Zulip Kenji Maillard (Jun 13 2020 at 14:01):

Is there such a thing as a "practical" type theory in that case ?
Or rather where is that essentially needed when we work with type theory ?

view this post on Zulip Kenji Maillard (Jun 13 2020 at 14:01):

Pierre-Marie Pédrot said:

but the stuff that says I don't know you never really know

Happens :shrug:

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 14:01):

I think this is entering the realm of philosophy

view this post on Zulip Kenji Maillard (Jun 13 2020 at 14:02):

please no, I meant on a practical ground

view this post on Zulip Kenji Maillard (Jun 13 2020 at 14:02):

In particular with respect to your earlier claim that computation was broken in some sense

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 14:03):

My claim is the following: in the "practical" type theory whatever it means, conversion incurs arbitrary needs of fuel

view this post on Zulip Kenji Maillard (Jun 13 2020 at 14:03):

100% Agreed

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 14:04):

So this means that you cannot really be sure about the validity of conversion

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 14:04):

so by reducing stuff you actually lose some bits of confidence

view this post on Zulip Kenji Maillard (Jun 13 2020 at 14:05):

You cannot be sure of the absence of conversion: is that used anywhere in type theory ?

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 14:05):

I don't think so, type theory should be monotonic w.r.t. conversion

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 14:05):

except that it's not clear with strict proposition

view this post on Zulip Kenji Maillard (Jun 13 2020 at 14:06):

Pierre-Marie Pédrot said:

except that it's not clear with strict proposition

how so ?

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 14:06):

I am not sure

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 14:07):

But the root of the undecidability is the fact that you can eliminate SProp Acc into Type

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 14:08):

In ETT, you're not monotonic because you can invoke conversions that have logical contents not present in the term

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 14:08):

For Lean, I don't know

view this post on Zulip Paolo Giarrusso (Jun 13 2020 at 14:36):

I knew somebody would bring up “decidable typechecking” as a practical problem, as if Coq commands were terminating in feasible time; and I don’t talk of Ltac loops, just of typeclass search and unification.

view this post on Zulip Gaëtan Gilbert (Jun 13 2020 at 14:40):

ETT looks monotonic AFAICT

view this post on Zulip Kenji Maillard (Jun 13 2020 at 17:31):

@Paolo G. Giarrusso In practice both Coq and Lean have similar practical limitations in their implementations. That's why I would like to understand better the theoretical consequences of a type theory where typechecking is only semi-decidable and not decidable.

view this post on Zulip Enrico Tassi (Jun 13 2020 at 18:54):

I could pass proofs from Coq to Matita and see the inability to type check them as a bug in Matita (or more interestingly a soundness bug in Coq)? If I try to write a third party checker for a tool based on an undecidable type theory, what can I really conclude from a failt to check?

view this post on Zulip Paolo Giarrusso (Jun 13 2020 at 19:01):

I assume Lean’s existing third-party checkers must use the same algorithm, and if a proof is rejected, you must fix it (like with Coq).

view this post on Zulip Enrico Tassi (Jun 13 2020 at 19:03):

As far as I know the importer from Lean to Coq turns conversion-checking off, right @Gaëtan Gilbert ?

view this post on Zulip Paolo Giarrusso (Jun 13 2020 at 19:04):

To me, the problem with undecidable type systems is how to formally test whether they’re “good enough” — clearly it’d be bad if the typechecker always looped, but that’s not what happens.

view this post on Zulip Enrico Tassi (Jun 13 2020 at 19:04):

Paolo G. Giarrusso said:

I assume Lean’s existing third-party checkers must use the same algorithm, and if a proof is rejected, you must fix it (like with Coq).

"third party" and "same algorithm" in the same sentence is funny ;-)

view this post on Zulip Paolo Giarrusso (Jun 13 2020 at 19:05):

Hm, same “actual” type system, at least.

view this post on Zulip Enrico Tassi (Jun 13 2020 at 19:05):

(we had for a long time an "independent checker" using "the same code" in Coq, so no pun intended)

view this post on Zulip Paolo Giarrusso (Jun 13 2020 at 19:06):

Has that changed now?

view this post on Zulip Enrico Tassi (Jun 13 2020 at 19:07):

no, but at least it is now documented as such I believe (CC @Maxime Dénès ), no claims of independence

view this post on Zulip Paolo Giarrusso (Jun 13 2020 at 19:08):

In Lean’s case, I guess you could formalize a translation from the “ideal” type system to the “actual” one (that adds more “annotations” of some sort), and inspect the translation (since it’s something the user might have to do on occasion)

view this post on Zulip Enrico Tassi (Jun 13 2020 at 19:08):

Today an independent checker would be Dedukti, there everything is very different!

view this post on Zulip Paolo Giarrusso (Jun 13 2020 at 19:10):

Dedukti + CoqInE if/when it’s completed, right?

view this post on Zulip Enrico Tassi (Jun 13 2020 at 19:11):

yes something like that. But my point was the independence, not the actual state of the tool

view this post on Zulip Paolo Giarrusso (Jun 13 2020 at 19:12):

Sure. On such a translation for Lean, I haven’t actually seen one for Lean, but it could probably be extracted from Carneiro’s master thesis with some work.

view this post on Zulip Gaëtan Gilbert (Jun 13 2020 at 19:27):

Enrico Tassi said:

As far as I know the importer from Lean to Coq turns conversion-checking off, right Gaëtan Gilbert ?

Not in general. It's pretty slow so turning conversion checking off is useful eg to see if it will bug on terms which depend on terms that don't reasonably-terminate, but it's meant to succeed even when checking conversion.

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 20:16):

you could formalize a translation from the “ideal” type system to the “actual” one

This is the way to justify ETT into ITT + UIP + funext, but there is something I judge wrong with that that I can't pinpoint

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 20:17):

because this translation is not compatible with reduction in the sense that if you reduce a term you don't necessarily know how to retrieve a correctness derivation for the reduced term

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 20:17):

I think that Théo Winterhalter's PhD has more formal complaints about this

view this post on Zulip Pierre-Marie Pédrot (Jun 13 2020 at 20:19):

so once again, if you only care about soundness this is moot


Last updated: Aug 19 2022 at 20:03 UTC