3 ms·

> This is similar to the case with many statically typed programming languages ... that have worse-than-exponential blow-ups in their type systems that essenti

by pron 6y ago

> This is similar to the case with many statically typed programming languages ... that have worse-than-exponential blow-ups in their type systems that essentially never show up in practice. I'm not so sure. Type checking/inference with "degenerate cases" (e.g. Hindley-Milner) is in FPT (fixed-parameter tractable) as are, AFAIK, all problems that are hard in the worst-case but could be easy in practice (e.g. SAT). Program analysis, (assuming "FSMification", of course, to avoid undecidability), was proven in 2005 to not be FPT. > Yes if you program in a fragment of a language you're fine. 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. > By this standard all programming languages are indistinguishable at a general level (which is true, but not very useful). 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. > Barring this, we have weak (but not unusually so for the field of programming) evidence, in the form of user communities of Turing-incomplete languages today, that people aren't generally creating heat-death style code on accident. Are you talking about niche languages (like configuration languages) or those intended to be general purpose? > The name of the game when creating programming languages is to target code that "a normal user would write." Completely restricting the entire language is just another lever in that process. Perhaps, but this claim requires evidence, unless we agree to keep it in the realm of art and aesthetics, which I'm more than happy to.

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

by pron 6y ago

6gvONxR4sf7o 6y ago

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.