3 ms·

> What's the complexity of that? Probably huge, but very reasonable for the subset of code people normally write (this again the analogy of Rice's theorem vs s

> What's the complexity of that? Probably huge, but very reasonable for the subset of code people normally write (this again the analogy of Rice's theorem vs static analyzers). I don't know off the top of my head, but I'm sure there's pathological cases that trigger cases where normalization becomes the same thing as full-on evaluation. But it doesn't show up in practice (see e.g. dhall as a working case), because you have to write pathological code. This is similar to the case with many statically typed programming languages (e.g. Java, Haskell, etc.) that have worse-than-exponential blow-ups in their type systems that essentially never show up in practice. I'm not sure any programmer alive has ever accidentally written a Java program that took days to compile (which could easily be possible with the right pathological behavior). EDIT: I forgot about Turing completeness in Java and Haskell's type systems; I meant leaving those tricks aside. > But that's often the case in Turing-complete languages, too. Moreover, the easy cases are usually not harder to detect in those languages. Yes if you program in a fragment of a language you're fine. We're trying to disincentivize users from stepping outside the fragment or at least let them be aware when that happens. One way of doing that is to make it off-limits to step outside that fragment. Another is a stratified language (e.g. Hume). Another way is an analyzer separate from the language. Yet another is community convention. > Any benefits can't be true in general because it is trivial to transform any program to an "effectively equivalent" FSM. By arguments analogous to this and the usual ones about Turing completeness this statement is always true in some form for any claimed benefit about any programming language. By this standard all programming languages are indistinguishable at a general level (which is true, but not very useful). > A claim that could be true is that in restricted languages, many more programs people write happen to be easier to analyse than the programs they would have written to do the same thing in an unrestricted language. That's certainly a very interesting empirical claim, but it requires empirical evidence. That is at the end of the day the contention behind any programming language. Yes I agree that this means that almost any proponent of a language talking about how it's "objectively" better is wrong. I also agree that this turns the entirety of programming languages into essentially an art-form rather than anything approaching a science. But such is the current state of things (yes also I happen to agree with your usual contention that this is a huge problem with the value proposition of PLT). 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. They're doing it on purpose to get around restrictions of the language. EDIT: 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.

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

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