4 ms·

I think you've swung way hard the other way. Specifically you're overlooking various classes of analysis that do get easier with more restricted languages and f

I think you've swung way hard the other way. Specifically you're overlooking various classes of analysis that do get easier with more restricted languages and focusing too hard on the general analysis of "let me prove an arbitrary statement about an arbitrary program" (i.e. the same pitfall people fall into when they point to Rice's theorem and say "ah so static analyzers are a worthless waste of time"). For example, with a strongly normalizing lambda calculus, I can prove intentional equality for any two functions and also have the nice property that extensional and intentional equality coincide. This means that I can prove e.g. that refactors that aren't supposed to change behavior in fact don't. A specific class of analysis to be sure that's not as useful as a general "prove anything about this function," but still quite useful. This specific property happens to be true of dhall. From the viewpoint of state machines, this is also true of FSMs. In that case, another way to think of it is that you get optimization for free. You can construct the minimal FSM with the same behavior as once you've created (this is also true for the lambda calculus case but generally it seems the lambda calculus isn't thought of usually in operational terms the same way FSMs are). Moreover, your last comment also illustrates that there are indeed classes of programs that are quite easy to analyze. When you say "many specific instances of programs" I presume you don't literally mean hard-coded single instances of a program, but rather classes of programs that all are structurally similar. These classes do not always align nicely along with the usual classes in theoretical CS, but that doesn't mean they aren't useful. For example a language consisting entirely of the holonomic functions with the usual semantics of them preserves symbolic integration, a nice little bit of analysis in the world of mathematical computing.

pron 6y ago
Just to be clear, I am not saying that very restricted languages in some very restricted domains (such as configuration or hypertext) are not useful. I'm saying that in general purpose languages, restricting the programming language is not a generally fruitful avenue if analysis and correctness are the goal. > For example, with a strongly normalizing lambda calculus, I can prove intentional equality for any two functions What's the complexity of that? > You can construct the minimal FSM with the same behavior as once you've created The complexity of that is more than linear in the number of states, that is usually at least exponential in the size of the program. > This means that I can prove e.g. that refactors that aren't supposed to change behavior in fact don't But that's often the case in Turing-complete languages, too. Moreover, the easy cases are usually not harder to detect in those languages. Any benefits can't be true in general because it is trivial to transform any program to an "effectively equivalent" FSM. 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.
- dwohnitmok 6y ago
  > 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

Just to be clear, I am not saying that very restricted languages in some very restricted domains (such as configuration or hypertext) are not useful. I'm saying that in general purpose languages, restricting the programming language is not a generally fruitful avenue if analysis and correctness are the goal. > For example, with a strongly normalizing lambda calculus, I can prove intentional equality for any two functions What's the complexity of that? > You can construct the minimal FSM with the same behavior as once you've created The complexity of that is more than linear in the number of states, that is usually at least exponential in the size of the program. > This means that I can prove e.g. that refactors that aren't supposed to change behavior in fact don't But that's often the case in Turing-complete languages, too. Moreover, the easy cases are usually not harder to detect in those languages. Any benefits can't be true in general because it is trivial to transform any program to an "effectively equivalent" FSM. 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.

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