Such a proposition pertains to a mathematical function. A running computer program does not contain mathematical functions, merely representations of them.
It is akin the difference between the theory of gravity and a falling rock. You can describe the rock with all manner of equations but you will not find any equations inside the rock.
A running computer program does not contain mathematical functions, merely represenations of them.
A printed computer program text does contain mathematical functions, and not merely representations of them.
Because of this difference, logical propositions about structures in the program text are types, whereas those about structures in the running program are not.
Furthermore, this has something to do with gravity and rocks: the running program is analogous to a falling rock, but the non-running program is like ... something else.
Somehow, compilers are exempt: they are running programs, which work with types. The source of this exemption is that they operate on other programs; a proposition inside a compiler is a representation about the program being compiled, not about anything in the compiler. Running programs may not entertain propositions about their own typing, because typing is purely prior to run-time. Type does not exist at run-time, period. The propositions of run-time typing are not type, but some kind system of data representations that mimics type.
Who decides these things? Some "world type authority"?