4 ms·

In your experience, what is the main impediment to proving properties of one’s code in Lean? Is it something specific to Lean or more generally an issue with th

by nequo 2y ago

In your experience, what is the main impediment to proving properties of one’s code in Lean? Is it something specific to Lean or more generally an issue with theorem provers?

ykonstant 2y ago
By far the main impediment is that the current community does not care about this use-case. Lean's proof system works mainly by using its metaprogramming aspects to write macro-type objects called tactics; they perform transformations on the goals of your proof to simplify or dispatch them. [Note that this meta-programming is very powerful, but also extremely hard to use from what I have managed to see; do not expect LISP style ergonomics here. It doesn't help that the meta-programming book shows some trivial examples of macro rules and then delves deep into proof tactics for the next 2 chapters, leaving the reader who wants general code transformations stranded]. In order to use Lean for proving properties for serious amounts of code, you need to write an entire tactics library similar to mathlib (but for code). Nobody has done this. Maybe it is reasonably hard, or maybe unreasonably hard; the point is, there is no serious collaborative effort that I know of.
- nequo 2y ago
  Do you get the sense that this would be easier with Coq due to the availability of suitable tactics? What makes you pick Lean instead of Coq for your projects?
  - ykonstant 2y ago
    Probably, from what people are telling me. But Coq is not a general purpose language, it is a dedicated theorem prover. I don't use Lean as a theorem prover for code (only for mathematics) and I myself don't do any code formalization unless someone offers to pay me. The reason I code in Lean is because I find it fun, and I think it is a very nice general purpose language; for instance, I like Lean much better than Haskell. If Lean ever gets the libraries Haskell has, I will be really excited.
    - Tainnor 2y ago
      I've only used Lean for proving maths theorems. What do you think makes Lean a better language than Haskell?
      - ykonstant 2y ago
        I prefer Lean to Haskell (never said Lean is a better language) for fairly shallow reasons really: - I like Lean's inductive type system much better that Haskell's, - I prefer eager evaluation by default, - I like the syntax better, - I like dependent types; they are dangerous, but it is great to have the option. I suspect some people may also prefer Lean's macro system to Haskell's, but I haven't worked much with either, so I don't know about that.
        Tainnor 2y ago
        Out of curiosity, have you tried Idris? It would tick at least boxes 2 and 4, while possibly being a little bit more geared towards general programming.

by nequo 2y ago

In your experience, what is the main impediment to proving properties of one’s code in Lean? Is it something specific to Lean or more generally an issue with theorem provers?

ykonstant 2y ago

By far the main impediment is that the current community does not care about this use-case. Lean's proof system works mainly by using its metaprogramming aspects to write macro-type objects called tactics; they perform transformations on the goals of your proof to simplify or dispatch them. [Note that this meta-programming is very powerful, but also extremely hard to use from what I have managed to see; do not expect LISP style ergonomics here. It doesn't help that the meta-programming book shows some trivial examples of macro rules and then delves deep into proof tactics for the next 2 chapters, leaving the reader who wants general code transformations stranded]. In order to use Lean for proving properties for serious amounts of code, you need to write an entire tactics library similar to mathlib (but for code). Nobody has done this. Maybe it is reasonably hard, or maybe unreasonably hard; the point is, there is no serious collaborative effort that I know of.

nequo 2y ago
Do you get the sense that this would be easier with Coq due to the availability of suitable tactics? What makes you pick Lean instead of Coq for your projects?
- ykonstant 2y ago
  Probably, from what people are telling me. But Coq is not a general purpose language, it is a dedicated theorem prover. I don't use Lean as a theorem prover for code (only for mathematics) and I myself don't do any code formalization unless someone offers to pay me. The reason I code in Lean is because I find it fun, and I think it is a very nice general purpose language; for instance, I like Lean much better than Haskell. If Lean ever gets the libraries Haskell has, I will be really excited.
  - Tainnor 2y ago
    I've only used Lean for proving maths theorems. What do you think makes Lean a better language than Haskell?
    - ykonstant 2y ago
      I prefer Lean to Haskell (never said Lean is a better language) for fairly shallow reasons really: - I like Lean's inductive type system much better that Haskell's, - I prefer eager evaluation by default, - I like the syntax better, - I like dependent types; they are dangerous, but it is great to have the option. I suspect some people may also prefer Lean's macro system to Haskell's, but I haven't worked much with either, so I don't know about that.
      - Tainnor 2y ago
        Out of curiosity, have you tried Idris? It would tick at least boxes 2 and 4, while possibly being a little bit more geared towards general programming.