alt Hacker News> A coworker recently remarked that lean seems like a new foundational language family that every programmer should be able to read, on par with C and Python, and I think it’s pretty hard to disagree with that.
Lean isn't super special in that regard. If you know Haskell or OCaml you are already pretty far along in at least being able to read Lean, as it comes out of a similar-enough tradition.
Replies
gf000 • yesterday at 8:10 AM
I would argue that it's pretty damn far from the Agda/Coq/lean world.
You really have to wrap your head around dependent types and _≡_. In my experience it was far more mind blowing than just FP.
➕ show 1 reply
> If you know Haskell or OCaml you are already pretty far along in at least being able to read Lean
But that's not really what you want, right? Speaking as a programmer, I'd think you would want a language where the prerequisite is "knowing a math proof", not "some mathey PL"
> every programmer should be able to read
You want "every math major should be able to read it", not "every programmer"