Why Lean?

Stream: Program verification

[Logan Murphy]

So as some may know I'm sort of beginning my first real research project by trying to use Lean for some assurance case verification. I'm at the point in the project where I have to decide whether I want to keep investing more time in Lean, or migrate to something like Coq, and to be able to defend my choice.

I'm still new to verification/FM, and my experience in Coq is limited to the first volume of SF, so I'm hoping I might be able to get some input from people with more experience in using theorem provers for verification. Does Lean have any advantages compared to Coq for this purpose? Does it have any technical disadvantages, aside from simply being a much younger system? What else would I probably want to consider in choosing between the two?

[Mario Carneiro]

If you are not planning to use an existing verification library or work with a team that already has a codebase, I think it's a pretty free choice. There is not any feature in either Coq or Lean which is specifically tuned for program verification

[Mario Carneiro]

but you can just do it like regular mathematics, with possibly a bit more inductive types than would be common in mathematics

[Simon Hudon]

As Mario says, the libraries can be a big factor. A lot of verification work has been done in Coq so the ecosystem there is richer. On my side, I prefer the tooling and language of Lean. The language, as you say, is younger. Whereas Coq got to explore the design space more (e.g. with canonical structures vs modules vs type classes), Lean committed right away to a design with type classes. I find that libraries are easier to write and use in Lean. You might want to discover for yourself how comfortable you are with the tooling and language and try solving the SF problems in Lean for comparison. (unfortunately, there's no complete draft of SF in Lean yet, it's still in progress)

[Mario Carneiro]

where is that draft?

[Simon Hudon]

https://github.com/alashworth/sf-lean/

[Jannis Limperg]

Lean's primary advantages, in my eyes, are much less idiosyncratic metaprogramming, mathlib and this chatroom. There are a few other differences (syntax, tooling, dependent pattern matching, definitional propositional extensionality, definitional reduction for quotients, pervasive use of classical logic, the handling of universes), but none of them strike me as particularly important.

So unless you plan to write complicated tactics or need the mathematics in mathlib, I'd go with Coq. It has less bugs, better reference and tutorial documentation, more libraries, more tactics and is generally much more polished. Lean is still very much in the research phase; particularly Lean 3, which will hopefully be obsolete soon.

[Johan Commelin]

Jannis Limperg said:

Lean is still very much in the research phase; particularly Lean 3, which will hopefully be obsolete soon.

Indeed, as soon as Lean 4 is released, we hope to continue our research phase there (-;

[Joe Hendrix]

The strengths of Lean for me have been easy metaprogramming, relatively easy to understand implementation, and C interop.