"type checking" would seem to be somewhat field dependent. aka treesitter for physics isn't exactly a direct reference to math[2][4].

Historically, checks for good/appropriate type impressions/groupings were not the responsibility of the blacksmith[0][1].

Physics drives math development via physics need to have math/mathematical explanations that correspond to physics observations/phenomina.

Type checking isn't a math thing, it's a make sure not mixing up math equations describing one type of physics phenominon are not mistaken/mixed up with/for unrelated type of physical phenominon. aka apples to oranges comparison. calculus reduces physics math complexity compared to algebra.

'pc world take' : cpu designer is not responsible for C language type mismatches. cpu implimentation can certainly make things easier/more difficult for C language comiler design/implimentation.

(sigh), not enough space for morse code/lambda calculus/(lisp/scheme) vs. (ascii/utf)/kleene*/(asm/C) discussion. Guess nod to Lewis Carrol "Through the Looking-Glass" will have to suffice.

------

[0] : https://letterpresscommons.com/type-founding/

[1] : linotype : https://blogs.loc.gov/headlinesandheroes/2022/06/the-linotyp...

[2] : intro to treesitter : https://tree-sitter.github.io/tree-sitter/

(missing apple reference)

[4] : niovim & treesitter : https://github.com/nvim-treesitter/nvim-treesitter