Lean 4.0.0, first official lean4 release

Re:Lean 4.0.0, first official lean4 release by nequo on Friday September 08, 2023 @03:25PM (#37438221)

I don’t think that your post is hostile. But from what I’ve heard, it is untrue because Lean 4 is intended to be a general purpose programming language, not only a theorem prover. I can’t find a source that directly states this goal but at the least this paper by Leo de Moura and Sebastian Ullrich presents it as a programming language:

https://link.springer.com/chapter/10.1007/978-3-030-79876-5_...

Microsoft also sponsored David Thrane Christiansen’s book, Functional Programming in Lean[1] (which I’m sure you know about!). That is another indication that they intend to reach programmers.

[1] https://leanprover.github.io/functional_programming_in_lean/

[ Parent | on HN ]

Re:Lean 4.0.0, first official lean4 release by sixbrx on Saturday September 09, 2023 @01:24PM (#37447774)

It seems general programming is more in focus now, but for context, the "Programming in Lean" book was only completed recently as compared to the multiple theorem proving documents which have been around for a while. The Christiansen book looks worth waiting for though and I really hope Lean can gain popularity as a general purpose language.

[ Parent | on HN ]