[jcburnham]

I think the same problems manifest in math, but to a different degree and in a different way. We do have some expectation of universal mathematics literacy, or at least math is a required subject in most schools around the world.

But I don't think that math education is generally very successful at teaching people math, as described in Lockhart's Lament: https://www.maa.org/sites/default/files/pdf/devlin/Lockharts...

My suspicion is that a big part of the issue is the way math is presented early on is really tedious and boring to a lot of people, in a way that could be addressed by theorem provers. I think something like the Xena Project https://xenaproject.wordpress.com/what-is-the-xena-project/ is potentially an interesting development in that regard (though more for undergraduate math than grade school math).

I also don't think this is anyone's "fault" really. I'm more interested in figuring out what might make things better than assigning blame. Nor do I think I personally can fix it single-handedly with a new programming language. If Yatima can move the ball forward a little bit by eventually contributing to a few people learning and falling in love with programming and math, that's more than enough for me.

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

[thyrsus]

One aspect of bad math education is that most folks competent in math can choose a different field than teaching and earn far more, without also figuring out how to motivate children while constrained by bureaucratized pedagogic dogma of the moment. Management is only sometimes a mob-of-children equivalent :-).