> 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"