Lean 4 + Exercism?

Stream: new members

[Isak Colboubrani]

Has there been any consideration of adding Lean 4 to Exercism? It seems like a structured and interactive platform like Exercism could be an excellent way for us to learn, practice, and collaborate on Lean 4 used as a programming language. NNG already covers the theorem proving aspect of Lean excellently!

For those unfamiliar, Exercism is a non-profit, open-source platform offering coding exercises across various languages, supported by a mentoring system where learners receive feedback from experienced practitioners. For more details see https://en.wikipedia.org/wiki/Exercism and https://exercism.org.

[Jon Eugster]

I believe as with many learning resources like this it's very much a question of funding and time.

I doubt that anybody would complain if somebody came along with enough time or resources to make something like that happen!

For example, NNG for Lean 4 is where it is because the university HHU and the German government (through Stiftung Innovation in der Hochschullehre) put quite some resources into it - and because of Kevin, who I believe also always got tons of support from Imperial College and grants from the UK government (?)

[Kevin Buzzard]

Is this any different to codewars? Someone put in a lot of effort to get Lean 3 supported there.

[Lukas Gerlach]

+1 on getting a Lean (4) track in Exercism!

What sets Exercism apart from platforms like codewars is the opportunity to get feedback from mentors for your implementations. Of course this requires a few people from the community to be willing to mentor solutions on the Lean track. I find this way of feedback incredible valuable from a student point of view because it can make you aware of features that you did not even know existed and it's a great way to learn interactively. (I've also done some mentoring work on the Crystal track, which is a great way to deeply learn a language as well.)

That said, reading a bit through https://exercism.org/docs/building/tracks/new, there are quite a few todos for setting up a new track. This also requires implementing a couple of standard exercises that exist on all tracks of Exercism.
In this way, an initial version of a Lean track would naturally emphasize the functional programming aspect rather than the interactive theorem proving aspect of Lean. This might be a valuable addition to existing resources like the Lean Games (e.g. NNG). Of course, apart from the standard exercises, any kind of exercise could likely be added if the exercism community is fine with that. This would potentially allow to dig deeper also into the theorem proving aspect.

I was tempted to just start building this track but I have the habit of starting too many projects at once so I'm not sure how much time I could really invest here, also because the track needs to be maintained in the long run.
If there are 1 or 2 people around who would like to share the effort in the long run (and ideally have some experience with Exercism from a student or mentor or maintainer point of view), I would be happy to initiate the first steps. (First of all, we would need to ask the Exercism community if they want such a track at all.)

Let me know what you think! :)

[Damiano Testa]

A lot of "mentoring" happens here, on Zulip: could questions be redirected here?

[Lukas Gerlach]

I guess putting links or letting people know that they can ask their questions here is always possible :)
One other point of mentoring is that people sometimes do not have very concrete questions but just submit a solution to an exercise and then want to know what can be done better or more idiomatic. I'm not aware to what extent this also happens in Zulip. If people already use Zulip heavily for this kind of "code review" then maybe the use of an Exercism track is limited (apart from reaching people not knowing about Lean yet).

[Damiano Testa]

I would say that a lot of this happens on Zulip. I also think that drawing on more people would be great, though!

[Lukas Gerlach]

Good to know, thank you! Then I'm not sure if it's really worth the effort...
I'll wait for a few more opinions :)