Lean as general purpose language?

Stream: new members

[mdioc]

Hey everyone, I stumbled upon Lean and was wondering, are many people using it for general programming tasks? I get the feeling most are utilizing it for theorem proving based on the docs but I was thinking about trying it out since it looks like a very interesting language. Any reasons not to give it an attempt? Thanks in advance!

[Jireh Loreaux]

Lean is definitely intended (and does) function as a general purpose programming language. There are plenty of people around who use it as such, although you are correct that there is also a very large theorem proving community too.

[Bulhwi Cha]

I don't think there are currently many people using Lean for general programming tasks. I want to try it in the future.

[Niels Voss]

I think Lean has roughly the same capabilities as Haskell in terms of general purpose programming, except Lean has also the ability to prove properties of your programs. There's definitely a lot of interest in this, but Lean 4 is still very young. Right now, most of the stuff written in Lean is intended to help the theorem proving community, although there's no reason you couldn't write a general purpose program in it. If you are interested in this, I recommend the book Functional Programming in Lean 4.

Some major projects written in Lean itself are:

• The Lean compiler and Lean package manager (lake) itself. Lean is a self-hosting compiler.
• Verso, a documentation authoring tool. I don't know much about this, but I think it turns Lean into a literate programming environment.
• A ray tracer.
• The tactics used by the theorem proving community are metaprograms written in Lean itself.
• Not sure if you would consider this general purpose, but there is SciLean for scientific computing.

[Kevin Buzzard]

Doesn't Amazon use it for Cedar?

[Henrik Böving]

Amazon has an implementation of Cedar in Lean but it is used as a target for differential fuzzing against the production version written in Rust. So while indeed fully functional it is not what is used productively.

[mdioc]

Excellent, thank you for the input everyone. I think I will give Lean a try on some small tasks and see how it goes. Verso also looks pretty neat.

[Kyle Miller]

In case you're interested, there were a few people doing Advent of Code in Lean last year (thread)

https://github.com/dupuisf/aoc2023
https://github.com/arthur-adjedj/AOC/tree/master
https://github.com/kmill/kmill-aoc2023
https://github.com/adomani/advents

[Edward van de Meent]

there also are some this year, and posting it in the discord

[Kyle Miller]

Niels Voss said:

I think Lean has roughly the same capabilities as Haskell in terms of general purpose programming, except Lean has also the ability to prove properties of your programs.

It's also got a very flexible built-in metaprogramming interface — for a small example application of it, in my AoC solution I set up a little system where my main function compiles a command line processor that dispatches to each days' solutions. It's something that you could whip up easily in Python with decorators, but I'm able to do this with a compiled language.

There are examples elsewhere of making mini-DSLs that you can embed inside the language. Even do notation, something that seems very core to Lean, could have been a user library(!).

It's all the fun of Lisp, but with syntax and types :-)

[mdioc]

That is a great explanation. To be honest, I am not certain I could really utilize even a fraction of what Lean can do but there is no better time to learn than now! I went ahead and started AoC as well just for fun. Will see how far I get :smile: I did find a few others that are doing AoC as well and I am reading over some other code to get an idea how to approach these problems in Lean. The Parsers seem really amazing

[Frédéric Dupuis]

Kyle Miller said:

In case you're interested, there were a few people doing Advent of Code in Lean last year (thread)

Also this year in my case: https://github.com/dupuisf/aoc24.

[mdioc]

Thanks for all the info. Decided to go for it and I managed to get day 1 done while looking to some others for inspiration. Learning functional programming is pretty challenging so any feedback is welcome! https://github.com/mdioc/aoc2024

[Marcelo Fornet]

I'm solving AOC this year for the first time in Lean :)

https://github.com/mfornet/advent-of-code-2024

[Yuri]

Kyle Miller said:

It's all the fun of Lisp, but with syntax and types :-)

This should be the Lean-as-a-programming-language tag line :-)

[Jason Rute]

I feel that tag line is true of basically every functional programming language except for Lisp.

[Kyle Miller]

That's far from my own experience @Jason Rute — what functional languages embrace metaprogramming as a core feature? (I haven't had a chance to use it, but Julia comes to mind as a possibility.)

[Mario Carneiro]

racket is the only other language I can think of that could be described as "embracing metaprogramming"

[Mario Carneiro]

but unfortunately even though it has syntax (that's kind of the whole point), it's still lisp-styled in the wild, in documentation, etc

[Mario Carneiro]

It reminds me of a scifi shapeshifter that goes around looking like a blob instead of a person because they have no particular reason to take a form

[Jason Rute]

@Kyle Miller I probably misunderstood what you meant by “syntax” then. (As for your metaprogramming question, maybe Scala 3. But again, I didn’t realize you meant syntax as in metaprogramming?)

[Mario Carneiro]

I think the metaprogramming part is coming from "all the fun of lisp"

[Luigi Massacci]

Mario Carneiro said:

It reminds me of a scifi shapeshifter that goes around looking like a blob instead of a person because they have no particular reason to take a form

I have to start using this metaphor :rolling_on_the_floor_laughing:

[Kyle Miller]

@Mario Carneiro I didn't mention Racket because it's "what if we started with Scheme and then went all-in on doing Lisp metaprogramming correctly". It's already too much of a Lisp, but it's diverged enough that it's worth mentioning.

@Jason Rute I'm not understanding what you're saying (what's "syntax as in metaprogramming"?). Maybe if your experience of Lisp is Scheme rather than Common Lisp what I'm saying doesn't make much sense, but, if you look at Lean closely, you notice that Lean.Syntax is essentially s-expressions, and it's a Lisp-with-a-surface-syntax like Dylan (which is actually a language that Sebastian looked at during the design of Lean 4). Both Lean and Common Lisp are extensible at a number of levels, but what I like about Lean is that you have access to a rich type theory to support more sophisticated metaprograms than you would ever dare to try writing in Common Lisp. I tend to feel you have a lot of freedom like in Common Lisp ("it's all the fun of Lisp"), and these two sorts of things are what I had in mind when I said it had syntax and types.