4 ms·

Same, I also found no good "for programmers" introduction.

crvdgc 3y ago
There is a short one[1] from Functional Programming in Lean, which is itself an introduction to Lean 4 from the programming's perspective. Highly recommended if you're interested in dependent types. [1]: https://leanprover.github.io/functional_programming_in_lean/introduction.html https://leanprover.github.io/functional_programming_in_lean/...
uxp8u61q 3y ago
Because the audience isn't "programmers".
- ykonstant 3y ago
  I think that is unnecessarily hostile; I believe Lean 4 can become a very capable programming language for mundane tasks!
  - uxp8u61q 3y ago
    Hostile? I just stated that the audience isn't programmers.
    - 7373737373 3y ago
      The age of guilds has long passed Are people like these not programmers? https://leandojo.org/ https://leandojo.org/
- siknad 3y ago
  How can the audience of a general-purpose programming language not be "programmers"?
- nequo 3y ago
  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_37 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/ https://leanprover.github.io/functional_programming_in_lean/
  - sixbrx 3y ago
    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.
agentultra 3y ago
https://agentultra.github.io/lean-4-hackers/ https://agentultra.github.io/lean-4-hackers/
- 7373737373 3y ago
  I'm not looking to use it as a programming language, but I'd like to see an introduction to theorem proving using Lean that is more explicit in its explanation of semantics than the ones that assume an existing math background
  - chabulhwi 3y ago
    Theorem Proving in Lean 4: https://leanprover.github.io/theorem_proving_in_lean4/ https://leanprover.github.io/theorem_proving_in_lean4/ I only had a basic knowledge of first-order logic and set theory before reading TPiL4. It wasn't easy, but now I can prove theorems in Lean. By the way, I still can't write a program in any language.

There is a short one[1] from Functional Programming in Lean, which is itself an introduction to Lean 4 from the programming's perspective. Highly recommended if you're interested in dependent types. [1]: https://leanprover.github.io/functional_programming_in_lean/introduction.html https://leanprover.github.io/functional_programming_in_lean/...

uxp8u61q 3y ago

Because the audience isn't "programmers".

ykonstant 3y ago
I think that is unnecessarily hostile; I believe Lean 4 can become a very capable programming language for mundane tasks!
- uxp8u61q 3y ago
  Hostile? I just stated that the audience isn't programmers.
  - 7373737373 3y ago
    The age of guilds has long passed Are people like these not programmers? https://leandojo.org/ https://leandojo.org/
siknad 3y ago
How can the audience of a general-purpose programming language not be "programmers"?
nequo 3y ago
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_37 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/ https://leanprover.github.io/functional_programming_in_lean/
- sixbrx 3y ago
  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.

agentultra 3y ago

https://agentultra.github.io/lean-4-hackers/ https://agentultra.github.io/lean-4-hackers/

7373737373 3y ago
I'm not looking to use it as a programming language, but I'd like to see an introduction to theorem proving using Lean that is more explicit in its explanation of semantics than the ones that assume an existing math background
- chabulhwi 3y ago
  Theorem Proving in Lean 4: https://leanprover.github.io/theorem_proving_in_lean4/ https://leanprover.github.io/theorem_proving_in_lean4/ I only had a basic knowledge of first-order logic and set theory before reading TPiL4. It wasn't easy, but now I can prove theorems in Lean. By the way, I still can't write a program in any language.