Lean and other languages

Stream: general

[Wrenna Robson]

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]

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]

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

[Wrenna Robson]

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

[Wrenna Robson]

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]

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

[Wrenna Robson]

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]

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]

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

[Wrenna Robson]

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]

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

[Reid Barton]

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

[Wrenna Robson]

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

[Reid Barton]

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]

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]

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]

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.