> I thought program analysis was just the attempts to infer/check properties of the program. It means to infer/check a property of the program: not of its str

> I thought program analysis was just the attempts to infer/check properties of the program. It means to infer/check a property of the program: not of its structure though (such as how many subroutines it has), but of its behaviour. > Nonetheless, the differences matter to people. But when people speak of terminating languages they hint at being interested at far "deeper" properties (not compositional, less local) than those that can be checked with a simple type checker. I am not claiming that languages don't matter, at least not here, only that termination doesn't help program verification (of the "deep" kind). > The scientific norm is decidedly NOT assuming one way or another prior to evidence/proof. If you make a claim that variable X has an effect on observation Y then the scientific norm is that while we don't know one way or another, the working hypothesis is that there is no effect, i.e. we give a preference to the assumption of no causal relationship between things. For example, we don't know whether or not eating lettuce on sunny Sundays increases baldness in men, but the scientific norm is that the working hypothesis is that it does not.