Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Functional Programming in Lean

leanprover.github.io

Post reply on HN
Print view View original

21–30 of 40 posts

Re: Functional Programming in Lean

#21

Post by siknad »

revskill wrote: post #16

Is this production ready ? How about performance (comparison with Rust)

Lean is currently moving to the 4th iteration which is the first intended to be a general-purpose programming language. It "is currently being released as milestone releases towards a first stable release". For now the main goal is to port mathlib to the new version, and then they will concentrate on the compiler. So it is not production ready. But that doesn't mean it is not suitable for building any programs now. There is a simple raytracer written in Lean [1]. I have built a chip8 interpreter with it and the only problem was the lack of an ecosystem, meaning I had to build the necessary libraries myself.

Now it has a RC GC and boxes everything >= 64 bits (including struct fields and IO/ST results), and as the compiler isn't polished it is probably significantly slower. In the referenced raytracer repo you can find rendering time compared to the C implementation (Lean is 25x slower, but that was a year ago).

[1] https://github.com/kmill/lean4-raytracer

Re: Functional Programming in Lean

#22

Post by d_christiansen »

mdm12 wrote: post #4
d_christiansen wrote: post #2

Lean 4 is an interactive theorem prover. It's also a programming language with a self-hosting compiler. This is a free book on using Lean 4 as a programming language, written without assuming any background in functional programming. It's intended to be accessible to Python, C#, Rust, Kotlin, Java, TypeScript, and Scala developers. Today marks the final release, after more than a year of writing.

Congratulations on the publication! As a dabbler in strictly typed functional programming languages like Scala and F#, I have always been curious about proof-oriented languages such as Coq or Agda, but found it difficult to justify the time investment. Lean seems to position itself as a theorem proving language that also supports general-purpose programs. Looking forward to digging into your book!

Thanks! I hope you find it valuable!

Those other languages are also definitely worth learning. Happily, there's lots of cross-transfer of ideas and skills between them, so learning one will make the others easier. I got my start in dependent types with Software Foundations and Coq, and that was very helpful when learning Agda and Idris later. Similarly, skills from them transferred quite readily to Lean.

Re: Functional Programming in Lean

#23

Post by d_christiansen »

ykonstant wrote: post #5
d_christiansen wrote: post #2

Lean 4 is an interactive theorem prover. It's also a programming language with a self-hosting compiler. This is a free book on using Lean 4 as a programming language, written without assuming any background in functional programming. It's intended to be accessible to Python, C#, Rust, Kotlin, Java, TypeScript, and Scala developers. Today marks the final release, after more than a year of writing.

Thank you very much for this book. It has been invaluable for my introduction to Lean and a joy to study from. I still have not read the last chapter, looking forward to it! Kudos for your effort, and I hope you will write some more stuff about Lean in the future.

Thank you for reading it, and I hope that the final chapter is also enjoyable for you. Right now, I plan to take a break - this book occupied every Saturday for about a year, and some time off is in order. But Lean is tons of fun, and I'd like to get back into it once I'm recovered a bit.

Re: Functional Programming in Lean

#24

Post by d_christiansen »

Reitet00 wrote: post #11
d_christiansen wrote: post #2

Lean 4 is an interactive theorem prover. It's also a programming language with a self-hosting compiler. This is a free book on using Lean 4 as a programming language, written without assuming any background in functional programming. It's intended to be accessible to Python, C#, Rust, Kotlin, Java, TypeScript, and Scala developers. Today marks the final release, after more than a year of writing.

This looks very nice! Is epub version planned?

Unfortunately not. I wanted to produce PDF and epub versions in parallel with the HTML version, but getting those to be of sufficient quality would have blown the time budget for the project. There's some old code in the Git history for dumping the source to Pandoc's dialect of Markdown, from which I was going to generate those, but the differences in Markdown dialects are enough that it was a fair bit of work.

Dropping a print version and focusing on epub could very well be faster, as I suspect that an mdbook->epub pipeline is less challenging than creating a quality print-ready PDF. But no plans right now.

Re: Functional Programming in Lean

#25

Post by d_christiansen »

theresistor wrote: post #17

I'm interested to know why I would want to learn Lean if I'm already familiar with Idris.

Lean occupies a different point in the design space. Its type theory is simpler and more conservative, its metaprogramming system is more reminiscent of Racket's (including hygienic procedural macros), and the focus on supporting professional mathematicians gives a different feel to the community and libraries. I think both are worth knowing, but either is great to learn. I hope the two projects learn more from each other in the future.

Re: Functional Programming in Lean

#27

Post by d_christiansen »

xigoi wrote: post #18
ggm wrote: post #7

Minor thing. Purely as a side: in C and C++, the conditional statement is written using if and else, while the conditional expression is written with a ternary operator ? and :. ending a sentence with . is a must. Including a period directly after a syntactic construct about ? and : is .. jarring because it is possible to attempt to read this as :. as an atomic construct in the language. Or even worse, the three-dots…

In the book, the ":" is typeset in monospace and the "." in proportional font, making their meaning clear.

I'm the author - I think that it's good to signal this kind of thing redundantly, and not rely on the details of typesetting to avoid confusion. I'll create an issue in the repo to rephrase the sentence.

Re: Functional Programming in Lean

#29

Post by d_christiansen »

ggm wrote: post #7

Minor thing. Purely as a side: in C and C++, the conditional statement is written using if and else, while the conditional expression is written with a ternary operator ? and :. ending a sentence with . is a must. Including a period directly after a syntactic construct about ? and : is .. jarring because it is possible to attempt to read this as :. as an atomic construct in the language. Or even worse, the three-dots…

I agree - this is inelegant. I'll make an issue in the repo to rephrase this sentence for the next time I do a round of typo fixes.

Thanks for the feedback!

Post reply on HN