Learning programming with lean 4

Stream: new members

[Aron Fischer]

Hi everyone,
I find myself interested in learning programming with lean 4. Are there any good resources to get started?
Specifically this is not a question about learning syntax but beyond that, how do you go about writing programs.

About me:
My background is in topology and category theory. Whenever I want to learn programming it goes like this: I start out with a python exercise, somehow find myself in Haskell a little while later, then I'm reading about idris, and then before long I'm reading about categorical logic... this is the basic trajectory every time.
last year I had a lot of fun going through lean 3 tutorials for theorem proving. Not using tactics, mind you, just writing proof terms. Really cool.

More recently I have been contributing to a python program again: 'manim'. This is a mathematical animation library used to make maths lecture videos. The videos it can make are great, but the language (python) is infuriating. I have been trying to add typing hints to it and clean up all the errors found by static type checkers ... but ... sigh.

I have gone through the MIT lectures on "Programming with categories". This is basically an explanation of how Haskell fits in with the simply typed lambda calculus and Cartesian closed categories. While fun lectures, they do not teach how to go about structuring a program, how to even start. When I go look at an open source Haskell project in the wild however, I usually find the code impenetrable. There are just too many programming constructs and conventions that I have not learned, not to mention the fact that programmers have their own vocabulary and jargon that partially overlaps with category theory jargon, but with different meanings for the same phrases.

All that is to say, I would love it if there were programming tutorials / exercises / cookbooks based on Lean 4. Where do I start?

[Kevin Buzzard]

Lean 4 isn't really ready yet. Are you absolutely sure you want to use Lean 4 rather than Lean 3?

[Aron Fischer]

I was under the impression that lean 4 is far more suited as a programming language than lean 3. At least that's what I gleaned from here: https://www.youtube.com/watch?v=UeGvhfW1v9M

While Lean 4 is not "ready" yet, I wouldn't mind starting out with it at this time. I don't urgently (or ever;) ) need it in production. For now, this is just for me.

Do you advise against it?

[Kevin Buzzard]

The unique resource to get started is the Lean 4 manual, which is unfinished (but there's a lot there): https://leanprover.github.io/lean4/doc/ . Other than that you can find lean 4 repos on github and try and learn from them, and also ask questions in the #lean4 stream. But the language is not stable yet -- we just have a couple of milestone releases.

[Kevin Buzzard]

Lean 3 there is a ton of documentation and information, and half a million lines of maths library to get you started.

[Kevin Buzzard]

Lean 3 -- if you want category theory, we got it. Lean 4, if you want category theory, you can start by defining a category yourself. Which of these is right for you depends on your use case.

[Aron Fischer]

Ah yes. I read that last night. It got me excited about this idea.
But those docs teach me syntax, not how to go about structuring a program.
Perhaps I should read tutorials for other languages (like haskell or idris) and try to use the those lessons here?

[Kevin Buzzard]

I am completely unclear about what you're actually trying to do so I'm not sure I can say any more unless you make your goals clearer. Hardly any programs have ever been written in Lean 4, and it has only existed in "preprint form" for a couple of months, so I would imagine that what a good Lean 4 program looks like right now is largely an unsolved problem, and indeed the answer may change over the next few months as the language itself changes.

[Kevin Buzzard]

Let me also stress that Lean 3 is also a programming language, and we have a really good idea of what a good program looks like in Lean 3. I don't really know what you think the difference is between Lean 3 and Lean 4 but until you really start getting into technical details the only differences really are some syntax changes and the fact that Lean 3 has half a million lines of maths library and a bunch of documentation whereas Lean 4 has the manual and essentially nothing else. Can you articulate why you think Lean 4 is suitable for what you want to do but Lean 3 is not?

[Aron Fischer]

Right. Perhaps I meant more in general: programming patterns in a language with such an expressive type system. Like, if the Haskell guides are about how to program in an environment based on the stlc, what is the corresponding thing for the calculus of inductive constructions?
It may be that such a thing doesn't exist. After all most people use Lean for proofs, and Haskell for general purpose programming. I'm curious about bridging that gap.
What am I trying to do? I'm not sure. I'm following my curiosity.

[Aron Fischer]

Can you articulate why you think Lean 4 is suitable for what you want to do but Lean 3 is not?

I guess I cannot.

[Kevin Buzzard]

Lean 3 is a functional programming language which you can use for general purpose programming, but it might not be fast because it is interpreted and not compiled (I am not a computer scientist, what I'm saying might not be quite true)

[Kevin Buzzard]

Whether this is an issue for you depends on what you want to do.

[Aron Fischer]

for now I just want to learn... so performance does not yet come into it.

[Kevin Buzzard]

If you watch Rob Lewis' videos on youtube -- look for the leanprover-community site and lean for the curious mathematician 2020 -- then you'll see how to write basic metaprograms in Lean 3. If you just want to experiment then Lean 3 might be the safest for now because there is a big crowd of people here who can answer your programming questions.

[Kevin Buzzard]

Lean 4 can be compiled into C and so will be a lot faster, but if speed is not an issue then why not start with Lean 3? If it becomes an issue you can just switch -- Lean 3 and Lean 4 are a bit like python 2 and python 3 -- different enough to make porting a large maths library difficult, but similar enough that working on one will teach you a lot of stuff which is common to both.

[Johan Commelin]

@Aron Fischer https://agentultra.github.io/lean-for-hackers/ might be interesting/relevant

[Adam Topaz]

Time to switch all my custom scripts to lean3 so I can back up my home folder with profinite sets

[Johan Commelin]

your home directory is a monad

[Adam Topaz]

Is that a nix thing?

[Yakov Pechersky]

Aron, since you mentioned manim, you might look into other languages/programming styles that are about declarative programming and functional programming. The best example of this, that I know of, in the context of getting data displayed visually is Elm: https://guide.elm-lang.org/core_language.html

[Yakov Pechersky]

There's also Functional Reactive Programming (FRP) that the Reflex library (https://reflex-frp.org/tutorial) in Haskell is great at

[Yakov Pechersky]

For general purpose programming in Lean[34], you can check out the robot the Galois guys made work with Lean 4: https://github.com/galoisinc/lean4-balance-car. It is a lot of IO and interop with C.

[Bryan Gin-ge Chen]

There are also some raytracers implemented in Lean 4.

[Aron Fischer]

great suggestions. thanks.

[Aron Fischer]

I have read the Elm docs. While cute, it is somewhat limited as a means of learning programming in a calulus-of-(inductive)-constructions setting. But it is clean and simple I enjoyed learning about it and it offers a lifeline to anyone stuck working in javascript and that is a commendable goal :)

I looked at the Lean-For-Hackers and tried to translate that into Lean 4 as an exercise. Hard work.... but I have an interactive hello world! (yay me)
The ray tracer and balancing bot too are cool, but of limited use to me at this stage.

I also found https://leanprover.github.io/programming_in_lean .. which sounded exciting, but sadly remains mostly unwritten.

I am wondering if perhaps this is the book I am looking for:
https://www.manning.com/books/type-driven-development-with-idris
It appears to teach the concepts needed to write and structure programs in idris, and hopefully a lot of that will translate to other languages. WDYT? Is that a good resource?

[Daniel Fabian]

I'd like to give a bit of a different perspective here. Whilst lean 4 is definitely nowhere nearly as polished on the UX side as lean 3, it is actually quite competent at being a programming language. The lean 4 compiler is written in lean 4 which is something that requires tons of the features a real-world programming language would need.

That said, it doesn't have a real packaging story so it's quite hard to get a real project going. But on the other hand the various syntactical tricks they've pulled makes writing monadic code (something you almost certainly need for anything non-trivial) very nice.

In fact, in a lot of ways it's quite a lot nicer than Haskell.

As a programming language it has a quite unique feel to it, since you can't debug anything, really, but you also tend to evaluate during type-checking time. So, in a sense, it almost feels like a dynamic language in a lot of ways.

If your goal is writing programs, lean 4 is actually a fine choice. Just don't expect you'll be writing many proofs. The tactics and library story is far behind what lean 3 + matlib can offer.

On the other hand, if you want to write some kind of program (especially hacking the lean 4 compiler itself), it's really good. You can still enforce some invariants at the type level if you are so inclined.

But the kinds of invariants you are more likely to express right now in lean 4 are kinds of things you want to carry around in your program. Perhaps, you'd like to prove that you are never going to access an array out-of-bounds. And then you can use that fact to make very efficient code. Stuff like that.

[Alex J. Best]

Daniel Fabian said:

but you also tend to evaluate during type-checking time. So, in a sense, it almost feels like a dynamic language in a lot of ways.

Can you say a bit more about what you mean here in these sentences? It sounds intriguing but I don't quite understand it, do you have an example?

[Daniel Fabian]

(These are not #mwe, I know. If you need one, let me know)

example motive n hn : @Power2ProofBelow motive n hn → Power2 n
  | Power2ProofBelow.base => Power2.base
  | Power2ProofBelow.ind hn h_motive => Power2.ind (by assumption)

Here's an example of the kind of thing you can do: This example is a pattern match, i.e. term mode, but then inside of the parenthesis, I create a tactic mode thing so I don't have to go and hunt for locals. If you put your cursor at a of assumption, you see the proof state.

Now the moment you make another tactic step, the proof state changes. It's a lot like having a debugger attached.

But this evaluation happens during type-checking time. At no point in time did you have to manually re-compile, or even run. The type checker runs (and executes your user code) with every key stroke.

So, it's almost like having a REPL open in JavaScript in that sense.

---

another example is this kind of thing:

def generateProofBelow (declName : Name) : TermElabM Unit := do
  if !(←isInductivePredicate declName) then
    let indInfo ← getConstInfoInduct declName
    let cmds := ←mkMutualBlock (←mkContext declName)
    trace[Meta.debug] "\n{cmds}"
  else
    trace[Meta.debug] "Not inductive"

#eval generateProofBelow ``Even

Now every time I change the code inside of generateProofBelow, it re-compiles the function, and re-evaluates it. So it's like re-running a debug session.