what advantages does lean have over f* and dafny?

Stream: Program verification

[Bulhwi Cha]

Bulhwi Cha said:

If I'm lucky, I'll be supported this summer or next year by NIPA's OSS Support Center (Open UP) to teach Korean students and programmers how to prove these string theorems.

The OSS Support Center has just requested me to submit a summary of the project I'll contribute to and a plan for my mentoring. They seem indifferent to formalizing mathematics, so I'll focus on explaining to them how Lean can be used in industry.

I wonder what advantages Lean has in program verification over proof-oriented programming languages like F* and Dafny. I don't know much about these two languages, but they appear more geared towards effectful programming:

• Section 20.5 of Proof-Oriented Programming in F* (last modified on Jun 25, 2024): https://fstar-lang.org/tutorial/proof-oriented-programming-in-fstar.pdf
• "Verification of Imperative Programs" (Dafny): https://dafny.org/teaching-material/Lectures/3-3-Verification-Imperative.html#/

[Bulhwi Cha]

Without a doubt, Mathlib is one of Lean's huge advantages; it's used in SampCert. But what else?

[Shreyas Srinivas]

1. Dafny has a larger trusted code base.
2. Working with dafny is not always a great experience because one must constantly massage the goals until the smt solver can tell you that you are fine. Since you don't get something like an infoview (there might be debugging tools I don't know), it is like having exactly one tactic. You must constantly supply the right amount of hints until this tactic can close the goal.
3. The more powerful the automation you use, the more mysterious and brittle the proof itself is. The proof can break because your goal stated the order of summands wrong or what not.

[Shreyas Srinivas]

I googled "dafny verification brittle" and landed at a blogpost that explains this aspect: https://dafny.org/blog/2023/12/01/avoiding-verification-brittleness/

[Shreyas Srinivas]

All that being said, dafny and F* have been used for a lot of verification papers in software. Lean also has a non trivial learning curve (although I think we get more info from the system when a goal is not closed)

[Shreyas Srinivas]

When mentioning mathlib as an advantage, you should probably explain which parts of mathlib were advantageous to sampcert. Maybe it was just what Mario calls Mathlib-lite. Or maybe it used deep mathematics theorems.

[Shreyas Srinivas]

Also @Mario Carneiro would have a better answer

[Shreyas Srinivas]

Another thing, since you mentioned effects, you can only put that sort of code into Dafny methods. These are not pure functions. But they are "opaque" in the system. There are some restrictions about putting methods inside another (iirc you just can't do that). They are purely visible as an interface with the requires and ensures clauses satisfied. I didn't work with dafny long enough to know how limiting this can be.

[John Tristan]

I find it difficult to choose between Lean and Dafny for teaching purposes. When I want to teach how to design and write proofs, I have a clear preference for Lean because I can present the rules of natural deduction and put them in practice. On the other hand, Dafny is nice and fun to teach how to verify programs by annotating them with invariants and learning about Floyd logic. However, a problem with tools based on SMT automation like Dafny is that as long as what you are trying to prove is simple enough, it feels like magic, but eventually you realize that you do need to know how to write proofs, and you don't have the interactive system and the proof scripts to help understand what is going on. Perhaps you should use both!

As for SampCert and its use of Mathlib, I don't know what qualifies as deep but here are three (plus 1 bonus) theorems I use. They may not be the deepest, but they're not high-school mathematics (at least not for me :smile: ). Overall, I felt like the most useful part of Mathlib for me was analysis.

1. Poisson summation formula
2. Jensen's inequality
3. Some convergence result of the Jacobi Theta function that, I think, saved me days of work proving what I want through simpler means
4. Finally, I'll mention a theorem that perhaps is not deep but that I found thanks to moogle.ai and that I was relieved to find because I felt stuck

[Bulhwi Cha]

John Tristan said:

As for SampCert and its use of Mathlib, I don't know what qualifies as deep but here are three (plus 1 bonus) theorems I use. They may not be the deepest, but they're not high-school mathematics (at least not for me :smile: ).

I'm pretty sure that the examiners of the OSS Support Center will regard these theorems as deep mathematics!

[Johan Commelin]

This is certainly not "mathlib lite".