> We do have some expectation of universal mathematics literacy, or at least math is a required subject in most schools around the world.
Certainly not to the degree required to use this programming language :)
> But I don't think that math education is generally very successful at teaching people math
I agree, but the most likely hypothesis that I am forced to adopt given the available evidence is that this has very little to do with how math is taught and a great deal to do with the fact that aptitude in many subjects is largely heritable.
I think there are serious benefits to be harvested from improved pedagogy, but almost entirely at the top end. A worthwhile goal, certainly, but only going to exacerbate the state of affairs you’re objecting to.
> I'm more interested in figuring out what might make things better than assigning blame
A worthwhile goal, but I don’t think a new dependently typed functional language is likely to cause any marginal changes in the direction you’ve stated a preference for. Probably the exact opposite direction, if anything.