This sounds like the idea that it's fine for C++ templates to not be typechecked, because the expanded template will eventually be checked by the compiler. Perhaps, but it makes for errors a long way away from their causes, which are difficult to debug.
If I ever divide by zero (or by something that might be zero) in my proof, I've almost certainly made a mistake. I'd rather hear about it straight away than later when I try to use some fact about the result of that division.
For completeness: C++ eventually introduced a feature to allow something analogous to type-checking for template metaprogramming, called concepts - https://en.wikipedia.org/wiki/Concepts_(C%2B%2B)
If I ever divide by zero (or by something that might be zero) in my proof, I've almost certainly made a mistake. I'd rather hear about it straight away than later when I try to use some fact about the result of that division.