learning lean first time

Stream: new members

[crab]

I have never worked with a dependently typed language before, but I do have experience with f#. would it be hard to learn lean?

[Henrik Böving]

Lean will most definitely feel quite different from F# but you will probably have an easier time than say a person who only knows java and python since F# has quite few functional concepts and constructs you won't see in those languages but all the time in lean (e.g. tagged union types, lots of recursion, pattern matching etc).

[Arthur Paulino]

Hm, I think it depends on what you consider "hard". I had never worked with a dependently typed language or anything like F# before and I could say it's being "hard" for me. But since I enjoy the challenge (and the elegance of Lean), it's actually being "emotionally easy", so to speak... in the sense that I feel very motivated

[Arthur Paulino]

And, of course, I have to mention the supportive Lean community here on Zulip :heart:

[crab]

Henrik Böving said:

Lean will most definitely feel quite different from F# but you will probably have an easier time than say a person who only knows java and python since F# has quite few functional concepts and constructs you won't see in those languages but all the time in lean (e.g. tagged union types, lots of recursion, pattern matching etc).

tbh I use recursion, pattern matching and tagged union types in f# a lot

[crab]

im could say im comfortable with them

[Henrik Böving]

Exactly and that's your advantage over people who are not familiar with functional languages and will definitely help you with learning Lean.

[crab]

cool

[Julian Berman]

For me (a Python programmer) learning Lean has been way more difficult than I expected. I can imagine you indeed have quite a leg up there like Henrik said.

[Yaël Dillies]

My own data point is that learning Lean was quite demanding, although I never got stuck.

[Henrik Böving]

I found most of the language relatively easy to learn but that is most likely because I already had experience with Isabelle/HOL and Haskell so I had to adjust rather small parts of my mental model to fit with Lean.

[crab]

I find lean 4 much more begginner friendly and f#-like than lean3

[crab]

Tho lean4 doesn’t have mathlib and still pretty new

[Henrik Böving]

We do have a (very very) partial port of mathlib already over at https://github.com/leanprover-community/mathlib4

[crab]

That’s amazing

[crab]

if i were to use lean, i would definitely use lean4, but i would like to wait a bit

[Henrik Böving]

I'd say if you have never worked in a dependently typed language before you can already go ahead and start learning with Lean 4, it takes a time to get used to and the final (semi automatic) full port of mathlib to Lean 4 will also happen in the not so distant future, maybe by the time you know all the basics it will already have happened^^

[crab]

Why in lean4 did they decide to make the syntax much more friendly?

[Arthur Paulino]

What do you mean? It came after Lean 3 so it's an opportunity to improve

[crab]

Did the community want to introduce less experienced programmers?

[Alex J. Best]

What do you mean by friendly?

[crab]

Syntax wise

[Alex J. Best]

Please elaborate on specific changes you want to know about? Whitespace sensitivity? Lack of commas?

[crab]

No, the whole syntax in general

[crab]

I honestly find lean4 syntax much more beginner friendly than lean3

[Julian Berman]

Then what do you mean by "why" :)?

[Julian Berman]

Usually that would mean you think it's worse to do so.

[crab]

I honestly think that it was a very good move, but I want to understand the motive

[Julian Berman]

I suspect making Lean 4 more accessible to a wider set of programmers was an explicit goal -- early on Leo de Moura mentioned one of Lean 4's objectives was to become a good general purpose programming language

[Julian Berman]

making the syntax similar to other languages helps there

[Huỳnh Trần Khanh]

from a programmer's perspective, when legacy code is so ugly and hard to maintain you just want to throw everything away and rewrite from scratch. Lean 3 has a lot of "legacy cruft" (performance gotchas, "excessive memory consumption", etc) and the devs are fed up, so they make a totally new and better Lean :joy:

[Arthur Paulino]

Lean Together 2021: An overview of Lean 4
https://www.youtube.com/watch?v=UeGvhfW1v9M

[Huỳnh Trần Khanh]

everyone has been in this situation at least once

[crab]

The errors?

[Huỳnh Trần Khanh]

yes. these random errors are the worst. this is why the devs make Lean 4 instead :joy:

[Patrick Massot]

@Huỳnh Trần Khanh you should really show a lot more respect towards Lean developers.

[Huỳnh Trần Khanh]

I do. in fact, writing a theorem prover or a programming language implementation is a huge undertaking and even experts get things wrong

[Patrick Massot]

What have you accomplished to feel so much superior?

[Huỳnh Trần Khanh]

no, I'm just saying that Lean 4 is a much better version of Lean. I really respect the devs :heart:

[Arthur Paulino]

From what I've noticed (and I'm a newbie here), there is quite a lot more involved in the creation of Lean 4 than the mere workaround of bugs. The whole infrastructure is much superior, more generic and more powerful. We have a server that implements LSP, we have an FFI, we have a cleaner syntax.

And I'm certain that it's still just the tip of the iceberg

[Henrik Böving]

All metaprogramming related stuff has drastically changed (in a good way)

[Huỳnh Trần Khanh]

yeah. and persistent data structures, mimalloc and functional but in place are just so cool. Lean 4 even beats Haskell :joy:

[Martin Dvořák]

You say that Lean 3 didn't beat Haskell?

[Henrik Böving]

Lean 3 was not capable of beating Haskell performance wise, the Lean 4 devs did invest quite a lot of time and research into novel techniques to outperform it.

[crab]

Some time ago, when I looked at lean 3, I honestly felt discouraged, but lean 4 is so much more welcoming and exciting. The devs really accomplished a great task

[Huỳnh Trần Khanh]

probably tangential but I hope there will be no Lean 5, just like Python 3 is the final version of Python :joy: and ES6 is the final version of JavaScript :joy: I honestly hope that the strategy that the devs use to implement Lean 4 is the best one for Lean :laugh:

and also to people who think that I disrespect Lean devs: I don't :joy: in fact after I replied to Crab's message I was already typing something along the lines of Lean is a complicated system and implementing it is hard and stuff, I didn't want to come across as being rude :joy: every complicated piece of software has a rocky start and Lean is no exception lol

[Patrick Massot]

Huỳnh Trần Khanh said:

Lean 4 even beats Haskell

I don't think writing such sentences helps at all. You should compare such a meaningless sentence to what is written in Section 8 of https://arxiv.org/abs/1908.05647 for instance. There you'll see very specific benchmark presented in a very careful way, explaining why results should be interpreted with caution.

[Patrick Massot]

I know research can seem less fun that internet trolling, but this is what we do here.

[Mario Carneiro]

By the way, in case you weren't aware @Huỳnh Trần Khanh , that screenful of random errors (which everyone has probably seen before) is a symptom of memory exhaustion. When the memory allocator starts to say "no" to things, almost every activity lean tries to do will fail, but because it is a resilient program it keeps going and throwing more errors. It is unlikely that lean 4 changes this, memory exhaustion is an extremely difficult situation to recover from

[Mario Carneiro]

That's also why restarting lean usually fixes the issue, because it frees everything and starts over. It is unclear whether this is even fixable; if there is a memory leak then this would be the usual way users will encounter it but that implication goes only one way - you can also genuinely run out of memory, and if for example you have (accidentally or otherwise) attempted to compile all of mathlib in RAM that might be a significant possibility.

[Kyle Miller]

@Huỳnh Trần Khanh I was under the impression that a reason Lean 4 has new code isn't because the Lean 3 code base is somehow unmaintainable, but rather one of the goals of the project is self-hosting: Lean 4 is designed to be capable of writing Lean 4 in Lean 4.

[Huỳnh Trần Khanh]

isn't self hosting a rite of passage for programming languages? a self hosted compiler is a great indicator of a language's maturity right? that is, if the Lean compiler, a big, nontrivial application can be written in Lean itself that it means Lean is mature enough to tackle real life applications?

[Arthur Paulino]

I don't see that link very clearly, but it definitely displays a certain level of maturity. And I also find it extra helpful because we can learn a lot about Lean 4 just from reading Lean 4 source code