Zulip Chat Archive

Stream: general

Topic: Lean and other languages


Wrenna Robson (Feb 24 2022 at 13:47):

Is there much written comparing and contrasting Lean (Lean 3 and Lean 4) with other similar theorem provers like Coq, or other general-languages-that-contain-theorem-provers like F*, or the wider zoo of Theoremy Stuff?

I'm currently trying to learn a bit of F* and it just seems horrible, conceptually, compared to the more elegant approach of Lean, but I'm sure I'm missing something. I'm looking for balanced thoughts on the different things that these different languages do well. I like Lean the most - but maybe I'm biased or wrong! It has been tricky to find discussion of serious comparisons though.

Mario Carneiro (Feb 24 2022 at 14:41):

I'm currently trying to learn a bit of F* and it just seems horrible, conceptually, compared to the more elegant approach of Lean, but I'm sure I'm missing something.

Could you elaborate on what seems horrible about F*? I can make some guesses but there are a lot of ways you could mean this.

Wrenna Robson (Feb 24 2022 at 17:39):

Oh, well, first off I find the whole "embed proofs into the types of definitions" thing... just very Ugh.

Wrenna Robson (Feb 24 2022 at 17:39):

I'm fundamentally happier with a paradigm where you define things, and then prove stuff about them.

Wrenna Robson (Feb 24 2022 at 17:41):

Sometimes, of course, a definition contains a proof - fine. But - to take the example they give in their manual - the idea that the type of a max function should include the assertion that it is indeed the max seems...

Wrenna Robson (Feb 24 2022 at 17:41):

I just don't understand what advantages are gained by doing things like that.

Wrenna Robson (Feb 24 2022 at 17:42):

Also in general I think it looks less nice than Lean, but that's really just syntax + syntactic sugar + Unicode support helping Lean.

Reid Barton (Feb 24 2022 at 18:23):

I don't know anything about F#, but a function like max is totally determined by its characteristic property and the particular implementation is irrelevant. The proof of correctness of the implementation is necessarily coupled to the implementation anyways, so you might as well do them at the same time and then create an abstraction boundary around them.

Reid Barton (Feb 24 2022 at 18:23):

For functions like addition of natural numbers, obviously that kind of thing doesn't make sense.

Wrenna Robson (Feb 24 2022 at 18:33):

F*, not F#. Agreed that the particular implementation is irrelevant, but the way Lean does this (you have a "default max" function, and then a linear order contains as part of its structure a different max function and a proof that it is equal to the default) makes much more sense to me. (Because the type of max is still α → α → α.)

Mario Carneiro (Feb 24 2022 at 18:39):

Since F* has subtyping, I think you can say the type of max is A -> A -> A too

Reid Barton (Feb 24 2022 at 18:41):

Oh I assumed we were talking about, say, the maximum of a list

Wrenna Robson (Feb 24 2022 at 18:41):

Yeah, I guess! I just find it much harder to read.

Reid Barton (Feb 24 2022 at 18:45):

Again I don't know much about F* (including the name, lol) but the fact that the max operation on an ordering is determined by the other structure is at the very least conceptually important--it means you don't have to worry about where the operation came from, or about keeping definitions of max coherent. In the Lean approach you just know it is a function, and then you have to worry about its definition and coherence and so on

Reid Barton (Feb 24 2022 at 18:53):

Anyways the main point is that "define things and then prove facts about them" is non-modular if you don't have some other form of discipline, since a proof about a definition is coupled to that definition.

Reid Barton (Feb 24 2022 at 19:03):

I think F* is mainly aimed at program verification, right? So then it makes sense that you would have a lot of functions like list.max that are intended to fulfill some given specification, and you want to treat them as opaque and not transparent.

Wrenna Robson (Feb 24 2022 at 19:17):

Reid Barton said:

Again I don't know much about F* (including the name, lol) but the fact that the max operation on an ordering is determined by the other structure is at the very least conceptually important--it means you don't have to worry about where the operation came from, or about keeping definitions of max coherent. In the Lean approach you just know it is a function, and then you have to worry about its definition and coherence and so on

We-ll, actually in Lean you know some of its properties inherently - but yeah this is essentially why F* does things that way I think.


Last updated: Aug 03 2023 at 10:10 UTC