3 ms·

I'm just butting into this conversation, but I think you're setting the bar to high. > Program analysis, (assuming "FSMification", of course, to avoid undecida

I'm just butting into this conversation, but I think you're setting the bar to high. > Program analysis, (assuming "FSMification", of course, to avoid undecidability), was proven in 2005 to not be FPT. I think your using "program analysis" in a different way than I'm used to. I thought program analysis was just the attempts to infer/check properties of the program. A property like termination and a property like "the type of this variable" are very different, obviously. What specifically are you referring to? > I'm claiming that analogous code to that which would be feasibly checkable in a restricted language would also be feasibly checkable in a non-restricted language, and that both are subject to the same difficulties. I mean, you're correct here, but missing the point. Consider a type checker, or Rusts borrow checker, or a side effect checker. The static analysis is going to be the same if you just translate the code to Python, for example. Nonetheless, the differences matter to people. I have a completely different confidence in my program's properties using somebody's pure function in Haskell than I do using some random Python function. If I looked at the source code, yeah I could reason through either of them in the same way, But in one, I don't have to. > Right, but that doesn't mean that a specific empirical claim should be assumed true until proven false, rather than the opposite, which is the scientific norm. A specific empirical claim should be suspected in whichever direction you personally think, given the arguments and incomplete evidence, held in a state of uncertainty until proven definitely one way or the other. The scientific norm is decidedly NOT assuming one way or another prior to evidence/proof.

pron 6y ago
> 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.

pron 6y ago

> 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.