It seems like this effort is going to increase a lot of overhead to do math, and obscures the role of thinking through the math conceptually. There seems to be a Principia Mathematica 2.0 idea in the programming world that we just need to reduce mathematics to code and it'll become easily accessible and usable. I'm not convinced that will be the case.