Development Background

Stream: new members

[Kristian Notari]

Hello everyone! I'm Kristian from Italy and I have a dev background, which turned to functional programming some months ago. I was looking for more pleasing ways of expressing my functional code and I've found Lean (and Idris, and Coq and a bunch of others). Lean seems pretty good at describing what you want in a clear way and more importantly in a readable way.

I've gone through the "Functional programming in Lean" book ('till chapter 3.3) and I'm interested in learning more.

Especially, I'd like to ask (1) what other resources are there for someone to learn how to approach general programming with Lean and (2) if graded modal types "à la" Granule are something describable within Lean.

Thanks!

[Tomas Skrivan]

There is https://agentultra.github.io/lean-4-hackers/ which talks about IO which is currently missing from FPiL.

[Kristian Notari]

Thanks! I'll take a look to it

[Jason Rute]

While it isn't about programming, some sections in TPiL might be more complete than FPiL. Also, I often find it helpful in programming to just get started trying to do stuff. So you could pick a set of learning problems like advent of code or your own personal project. A lot of stuff in Lean 4 isn't documented (or worse is changing), but if you look at the code, you can find a lot by looking how things are done there. Also https://leanprover-community.github.io/mathlib4_docs/ is useful.

[Jason Rute]

And I assume you know about the manual: https://leanprover.github.io/lean4/doc/whatIsLean.html

[Kristian Notari]

I know about TPiL (reading it now), FPiL (already read) and the manual (which I've kept as a go to reference in case I needed it).

You're right, I should probably start doing something then see where I end up. Thanks for the advice!

[Tomas Skrivan]

I have learned a huge amount just by reading Lean 4 source code. For example, use go to definition editor command on Nat, this takes you to the Lean's source code. Then use find references on the succ constructor and voila you can have a look at every single use case of Nat.succ. (finding references of a symbol is a recent lsp addition, right? I don't remember it working in the past)

[Taro Naoi]

Reading through https://github.com/leanprover/std4(collection of data structures and tactics written in Lean4) and https://github.com/leanprover/lean4-samples(collection of Lean4 code samples) and reimplementing some of them might be a good exercise to check your understanding of the language.

[Kristian Notari]

Thanks to both of you. I'm certainly trying your advices