As far as the computer is concerned, a program is just a list of instructions. Not even functions of type `nat -> nat` exist at that level. However, that isn't

As far as the computer is concerned, a program is just a list of instructions. Not even functions of type `nat -> nat` exist at that level. However, that isn't a very convenient way to program, which is why high-level programming languages exist. As far as a typed high-level programming language is concerned, a syntax tree that doesn't type check isn't a program, so the question of what it does at runtime is simply ill-posed.