ps. and our calculators (& excel) needs better support for it
Did your highschool physics not have this? I always thought it was a universal part of all physics education. Doing things like canceling out units etc. has always been a big part of high school physics, and checking that your final answer has the units it should. (If it didn't, you made a mistake somewhere.)
The idea of building units into Excel is definitely an intriguing one, though. I'm honestly kind of surprised it's the first time I've ever heard it suggested. It does seem like a pretty useful idea.
Gotta love that USA's 'A'P classes' entire curriculum are Chapter 1, p.1 everywhere else.
I can't imagine any HS science class not already doing this. It would be impossible to answer many, if not all, of the questions correctly if you mix units (either unit-kind like mixing time and distance units, or unit-scale like mixing seconds and hours).
Your point about tools that support units is great. Reminds me of https://frinklang.org/
For example, what is the type of the / operation such that 4m/2s = 2m/s, but also 4kg/2kg = 2?
It's not impossible of course, but it is highly tedious and complex to actually define these types in a formal way.
Not to mention, linear algebra (matrix operations) gets REALLY ugly to define formal types for really fast if you allow different measurement units for every matrix element, like you often do in physics.
And, just like the others, I never met a physics class that didn't enforce unit maths at every step of computation, starting in sixth grade.
But this is done with a simple informal system, not type theory of all things. The informal system of measurement units being essentially to treat the units as special values that act as factors and obey all the usual rules of multiplication and division, and don't allow addition or subtraction.
Types as such are dealt with as sets. So for example I'm working my way through Serge Lang's "Basic Mathematics" at the moment[1], and it starts with the natural numbers, then the positive integers, then the integers, then the rational numbers, then the reals etc. This is very normal for high-school level maths education.
I believe that mathematically the formal theory of types comes from a different branch from sets which arose when Russel attempted to address the problems caused by his paradox. "Type" theory was part of Russel's solution whereas Zermelo Fraenkel set theory is where everyone else felt that sets just needed a little patch to carry on working pretty much as before.
[1] Which I'd really recommend for anyone who wants a maths refresher that starts from very basic concepts but really challenges you to think like a mathematician, prove things etc. So in the first chapter when you only know the distributive and associative properties he has you using them to prove stuff.