[wyager]

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