Hah! No wonder you don't grok my perspective.
If you derive a C++ compiler that accepts file A as valid C++. And I derive a C++ compiler that rejects file A as valid C++, then from the lens of type theory the two compilers have different type-signatures!
They are not the same formal language. One, or both compilers implement a language that is not C++.
Perfect!
Please produce a piece of code (in a language such as Coq or Agda) which proves whether any given piece of random data has the type “C++ compiler” or “C++ program”.
That is the epitome of static type-checking, right?
C++ the language very much does tell you what to expect at runtime, though perhaps not everything you could ever want. I mean, it's not Haskell or Idris with their much richer type systems.