10 ms·

I understand that Turing completeness is not always a desirable quality for your programming language of choice, but since it is a rather obscure thing for thos

I understand that Turing completeness is not always a desirable quality for your programming language of choice, but since it is a rather obscure thing for those of us who haven't studied CS, when is a non-turing-complete language a favorable choice compared to a more traditional turing complete one?

TeMPOraL 9y ago
Security. A lot of security vulnerabilities in programs essentially boil down to your code being an ad-hoc parser for an (often implicit) language that's more powerful than you wanted. Turing-completeness is especially dangerous, and you want to avoid it if you don't actually need it. This is a very insightful way of looking at things, and is a research area called langsec. See: - http://langsec.org/ http://langsec.org/ - Papers and public talks of Meredith L. Patterson - https://www.gwern.net/Turing-complete https://www.gwern.net/Turing-complete for some examples of unexpected Turing-completeness
- chriswarbo 9y ago
  > Turing-completeness is especially dangerous, and you want to avoid it if you don't actually need it. Can I ask why Turing-completeness is "especially dangerous"? Let's say we have a pure language for e.g. generating a JSON value (nested lists/maps of strings, floats, nulls and booleans). It has no primitives other than null, true/false, string, float, list, map and function literals, and corresponding "arithmetic" functions for each type. What would the safety and security differences be between such a language being Turing-complete and not being Turing-complete? Programs in these languages can't "do" anything, other than calculate. The only problem I can think of is making denial-of-service easier, by e.g. generating an infinitely large list and running out of memory: (\x -> [ null ] ++ (x x)) (\x -> [ null ] ++ (x x)) This will generate `[ null, null, null, ... ]` until it runs out of memory. However, we could still blow the memory without Turing-completeness, e.g. by growing an exponentially large datastructure for a large number of steps (basically like a zip bomb): (\f xs -> case xs of nil -> [ null ] (cons y ys) -> (f f ys) ++ (f f ys)) (\f xs -> case xs of nil -> [ null ] (cons y ys) -> (f f ys) ++ (f f ys)) [ null, null, null, null, null, ...and so on 1000 times ] This recursion is well-founded, and structurally-decreasing since we only call `f` with a strictly-decreasing value of `xs`, until we hit the base-case for `xs = nil` where we return `[ null ]`. In the non-base-case we recurse twice to generate two identical lists, then append them together. This results in a list with 2^1000 elements, easily consuming all available memory. Hence for security, we need to kill programs which go over some predefined time/memory bounds regardless of whether or not they're Turing-complete. Hence my question about whether or not Turing-completeness is "especially dangerous", in comparison to e.g. I/O primitives.
  - Gabriel439 9y ago
    The latter example you gave will still not type-check in Dhall, although I'll still answer the spirit of your question You can write expressions in Dhall that will take a long time to evaluate (see the Ackerman example elsewhere in this thread), but it's harder to do so by accident. Totality checking is worthwhile for the same reason that seatbelts are worthwhile: they don't protect against all accidents, but they do protect against a lot of them
    - chriswarbo 9y ago
      > Totality checking is worthwhile for the same reason that seatbelts are worthwhile: they don't protect against all accidents, but they do protect against a lot of them Don't get me wrong, I'm all in favour of totality! My question was mostly about the "especially dangerous" wording. In my opinion, the major advantage of using Dhall for config instead of say, Scheme, is that it's pure/referentially-transparent/has-no-IO/etc., which everyone seems to be ignoring in favour of debating whether or not totality is desirable (Of course, Dhall does have "I" (but not "O") in the form of imports, but these are "morally pure" as long as URL contents are stable, similar to Nix's imports being "morally pure" as long as builds are deterministic). > The latter example you gave will still not type-check in Dhall Incidentally, how does Dhall check for totality? I know it's based on the calculus of constructions; does it use syntactic guardedness checks like Coq? Whilst I like totality, I'm still undecided about whether it's worth enforcing in general-purpose languages (e.g. Agda, rather than Dhall), since totality checking is still quite restrictive. The usability balance for static typing was crossed by Hindley-Milner, but I'm yet to see such an unobtrusive approach to totality checking (whenever my Coq or Agda projects become more than toys, they tend to get wrapped up in a monadic `Delay` to avoid fighting things like syntactic guardedness!)
      - Gabriel439 9y ago
        Dhall does the dumbest thing possible to enforce totality: Dhall doesn't support recursion! Note that Dhall does support lists and folds on lists (which are total), but not user-defined recursion For example, if you write: let x = x in x ... then the second `x` will be flagged as an unbound variable because `let`-bound variables are not in scope for their own definitions. Similarly, there is no `let rec` in Dhall That implies that if you want a user-defined recursive type that was not a list then you have to explicitly Boehm-Berarducci-encode the recursive type and its inhabitants. For example, if you wanted to encode the following Haskell data type in your configuration: data Tree = Node Integer | Branch Tree Tree example :: Tree example = Branch (Node 1) (Branch (Node 2) (Node 3)) ... you would encode it like this: λ(Tree : Type) → λ(Branch : Tree → Tree → Tree) → λ(Node : Integer → Tree) → Branch (Node 1) (Branch (Node 2) (Node 3)) You can think of Boehm-Berarducci encoding as "anonymous recursion" when you write it this way because every inhabitant of such a "recursive" type includes the datatype definition in the value (if you view the lambda-bound type and constructors as the datatype definition) Or to put it another way, if you ignore Dhall's support for builtin types, builtin functions, and imports then Dhall is literally the exact same thing as System Fw . You're used to thinking of System Fw or the calculus of constructions as underlying core languages for a higher-level language semantically defined in terms of the core language like Coq, Agda or Haskell. However, in Dhall there is no underlying core language: you are assembling raw System Fw expressions. Since the most pedantic definition of System Fw requires explicit polymorphism and doesn't support recursion then Dhall behaves the same way, too. I agree, though, that the lack of (unsafe) IO is an even bigger deal. Like you mentioned, if you use immutable URLS (such as IPFS) then they are basically pure. Even if you do use mutable URLs, you can always use the ability to normalize programs to purify them of imports (and you can also use Dhall's API to safely and statically verify that an expression is devoid of imports).
qznc 9y ago
Other popular non-Turing-complete languages are TeX and SQL. In practice, the fact that the program cannot hang is probably the biggest point. Every programmer has experienced bugs where the program runs into an infinite loop or deadlocks. Those are the nastier bugs. Removing Turing-completeness removes that whole class of bugs, similar to how Rust removes the whole class of data race bugs.
dozzie 9y ago
For configuration you very much do not want Turing-complete language -- or any programming language, for that matter. Configuration quite often is processed by more than just the original program it was intended for, so plain data dump is the easiest form from this angle. Also, it's much easier for human operator to just read the values than to interpret a de facto script that produces values. There were several attempts at using a programming language the tool was written in for storing its configuration. None worked well enough to catch up as a general trend, and not because the languages used were Turing-complete. My opinion is that a programmer has seen for a short moment what sysadmins do and decided to make something to help in the task, without really understanding what's needed and what works, what doesn't work, and why.
lmkg 9y ago
If your language is not Turing Complete, then it might be possible to always prove certain properties of programs. Canonically, you might be able to prove that the program will always complete and exit in finite time on any input. Other properties include guaranteeing that an error will not be thrown (or will be thrown), or bounding the amount of time or memory consumed, or guaranteeing that the output of a function will be within a certain numeric range.
tincholio 9y ago
For instance, if you want to make guarantees about program termination (as the author does here). This is not possible for Turing complete languages.
chowells 9y ago
You would always prefer to not have Turing completeness in your language, all other things being equal. Turing completeness isn't ever necessary to write the logic you want to write. But all other things are not equal. There is a cost to giving up Turing completeness. The language must now ensure additional properties about the code, mostly related to termination and productivity. The two strategies for this are reducing functionality offered by the language until you can prove all programs are good and introducing tools into the language to write compiler-verified proofs about your code. Dhall is an example of the former approach. It removes enough pieces that it can only express computations that terminate. Language like Idris, Agda, and Coq are examples of the latter. They provide rich systems that allow you to express proofs of various properties as needed to avoid Turing completeness. Both categories of language are currently difficult to use for general purposes software. Turing completeness is a sacrifice made to ease writing software at the cost of making certain bugs possible. At the moment, the best times to use a non-Turing complete language are when you have a problem domain where you can be satisfied with a reduced power language, or when you want to go all the way in the opposite direction and write machine-checked proofs about your software. As we study these things more, we find ways of easing the burden of using languages that aren't Turing complete. Maybe in the far future, systems will be good enough that most software can comfortably be written in languages that aren't Turing complete. It's a worthy aspiration. It's not now, though.
RodgerTheGreat 9y ago
In layman's terms, it is impossible to determine certain properties of an arbitrary program written in a Turing-complete language. Properties like "will this program finish within a reasonable amount of time?" or "does program X do the same thing as program Y?" For a non-turing-complete language, it may be possible to test such properties. It's crucial to understand that this distinction is not one of how practical it is to determine properties; once you open the door to Turing-completeness, all ability to reason about a program effectively flies out the window. You might be able to come up with rules-of-thumb that determine an interesting property of a program in a Turing-complete language some of the time, but there will always exist programs for which your rules-of-thumb are insufficient.
Gabriel439 9y ago
Here's a practical example of why it's beneficial to not be Turing complete. In Dhall, you can normalize programs, even if they are functions. For example, the interpreter can automatically simplify this Dhall function: let replicate = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate in let exclaim = λ(t : Text) → t ++ "!" in λ(x : Text) → replicate +3 Text (exclaim x) ... to this one: λ(x : Text) → [x ++ "!", x ++ "!", x ++ "!"] ... even though we haven't applied the function to any arguments yet. You can't perform this sort of simplification (in general) if the language is Turing-complete This sort of automatic simplification comes in handy a lot when authoring configuration files. For example, if somebody objects to the import of the remote `replicate` function, you can just simplify the file and (voila!) all the imports are gone because they've all been inlined and reduced. Similarly, if somebody objects to excessive use of abstraction and functions you can similarly simplify them to remove all indirection
- skybrian 9y ago
  This is inlining a function and unrolling a loop. It's done in many languages, no? More generally, many automatic refactorings are not entirely safe but we do them anyway, assuming that the code will terminate (since intentional infinite loops are rare) and relying on tests and human reviewers to check for mistakes. Depending on the program, substituting equals for equals might have to be rolled back for performance reasons; computing a mathematically equal value is no guarantee.
  - Gabriel439 9y ago
    In a Turing complete language you can't safely inline all functions to completion without risking an infinite loop. In such a language there is no decidable way to know when to stop inlining things
    - skybrian 9y ago
      It doesn't matter in practice, because we don't need to inline every function.

TeMPOraL 9y ago

Security. A lot of security vulnerabilities in programs essentially boil down to your code being an ad-hoc parser for an (often implicit) language that's more powerful than you wanted. Turing-completeness is especially dangerous, and you want to avoid it if you don't actually need it. This is a very insightful way of looking at things, and is a research area called langsec. See: - http://langsec.org/ http://langsec.org/ - Papers and public talks of Meredith L. Patterson - https://www.gwern.net/Turing-complete https://www.gwern.net/Turing-complete for some examples of unexpected Turing-completeness

chriswarbo 9y ago
> Turing-completeness is especially dangerous, and you want to avoid it if you don't actually need it. Can I ask why Turing-completeness is "especially dangerous"? Let's say we have a pure language for e.g. generating a JSON value (nested lists/maps of strings, floats, nulls and booleans). It has no primitives other than null, true/false, string, float, list, map and function literals, and corresponding "arithmetic" functions for each type. What would the safety and security differences be between such a language being Turing-complete and not being Turing-complete? Programs in these languages can't "do" anything, other than calculate. The only problem I can think of is making denial-of-service easier, by e.g. generating an infinitely large list and running out of memory: (\x -> [ null ] ++ (x x)) (\x -> [ null ] ++ (x x)) This will generate `[ null, null, null, ... ]` until it runs out of memory. However, we could still blow the memory without Turing-completeness, e.g. by growing an exponentially large datastructure for a large number of steps (basically like a zip bomb): (\f xs -> case xs of nil -> [ null ] (cons y ys) -> (f f ys) ++ (f f ys)) (\f xs -> case xs of nil -> [ null ] (cons y ys) -> (f f ys) ++ (f f ys)) [ null, null, null, null, null, ...and so on 1000 times ] This recursion is well-founded, and structurally-decreasing since we only call `f` with a strictly-decreasing value of `xs`, until we hit the base-case for `xs = nil` where we return `[ null ]`. In the non-base-case we recurse twice to generate two identical lists, then append them together. This results in a list with 2^1000 elements, easily consuming all available memory. Hence for security, we need to kill programs which go over some predefined time/memory bounds regardless of whether or not they're Turing-complete. Hence my question about whether or not Turing-completeness is "especially dangerous", in comparison to e.g. I/O primitives.
- Gabriel439 9y ago
  The latter example you gave will still not type-check in Dhall, although I'll still answer the spirit of your question You can write expressions in Dhall that will take a long time to evaluate (see the Ackerman example elsewhere in this thread), but it's harder to do so by accident. Totality checking is worthwhile for the same reason that seatbelts are worthwhile: they don't protect against all accidents, but they do protect against a lot of them
  - chriswarbo 9y ago
    > Totality checking is worthwhile for the same reason that seatbelts are worthwhile: they don't protect against all accidents, but they do protect against a lot of them Don't get me wrong, I'm all in favour of totality! My question was mostly about the "especially dangerous" wording. In my opinion, the major advantage of using Dhall for config instead of say, Scheme, is that it's pure/referentially-transparent/has-no-IO/etc., which everyone seems to be ignoring in favour of debating whether or not totality is desirable (Of course, Dhall does have "I" (but not "O") in the form of imports, but these are "morally pure" as long as URL contents are stable, similar to Nix's imports being "morally pure" as long as builds are deterministic). > The latter example you gave will still not type-check in Dhall Incidentally, how does Dhall check for totality? I know it's based on the calculus of constructions; does it use syntactic guardedness checks like Coq? Whilst I like totality, I'm still undecided about whether it's worth enforcing in general-purpose languages (e.g. Agda, rather than Dhall), since totality checking is still quite restrictive. The usability balance for static typing was crossed by Hindley-Milner, but I'm yet to see such an unobtrusive approach to totality checking (whenever my Coq or Agda projects become more than toys, they tend to get wrapped up in a monadic `Delay` to avoid fighting things like syntactic guardedness!)
    - Gabriel439 9y ago
      Dhall does the dumbest thing possible to enforce totality: Dhall doesn't support recursion! Note that Dhall does support lists and folds on lists (which are total), but not user-defined recursion For example, if you write: let x = x in x ... then the second `x` will be flagged as an unbound variable because `let`-bound variables are not in scope for their own definitions. Similarly, there is no `let rec` in Dhall That implies that if you want a user-defined recursive type that was not a list then you have to explicitly Boehm-Berarducci-encode the recursive type and its inhabitants. For example, if you wanted to encode the following Haskell data type in your configuration: data Tree = Node Integer | Branch Tree Tree example :: Tree example = Branch (Node 1) (Branch (Node 2) (Node 3)) ... you would encode it like this: λ(Tree : Type) → λ(Branch : Tree → Tree → Tree) → λ(Node : Integer → Tree) → Branch (Node 1) (Branch (Node 2) (Node 3)) You can think of Boehm-Berarducci encoding as "anonymous recursion" when you write it this way because every inhabitant of such a "recursive" type includes the datatype definition in the value (if you view the lambda-bound type and constructors as the datatype definition) Or to put it another way, if you ignore Dhall's support for builtin types, builtin functions, and imports then Dhall is literally the exact same thing as System Fw . You're used to thinking of System Fw or the calculus of constructions as underlying core languages for a higher-level language semantically defined in terms of the core language like Coq, Agda or Haskell. However, in Dhall there is no underlying core language: you are assembling raw System Fw expressions. Since the most pedantic definition of System Fw requires explicit polymorphism and doesn't support recursion then Dhall behaves the same way, too. I agree, though, that the lack of (unsafe) IO is an even bigger deal. Like you mentioned, if you use immutable URLS (such as IPFS) then they are basically pure. Even if you do use mutable URLs, you can always use the ability to normalize programs to purify them of imports (and you can also use Dhall's API to safely and statically verify that an expression is devoid of imports).

qznc 9y ago

Other popular non-Turing-complete languages are TeX and SQL. In practice, the fact that the program cannot hang is probably the biggest point. Every programmer has experienced bugs where the program runs into an infinite loop or deadlocks. Those are the nastier bugs. Removing Turing-completeness removes that whole class of bugs, similar to how Rust removes the whole class of data race bugs.

dozzie 9y ago

For configuration you very much do not want Turing-complete language -- or any programming language, for that matter. Configuration quite often is processed by more than just the original program it was intended for, so plain data dump is the easiest form from this angle. Also, it's much easier for human operator to just read the values than to interpret a de facto script that produces values. There were several attempts at using a programming language the tool was written in for storing its configuration. None worked well enough to catch up as a general trend, and not because the languages used were Turing-complete. My opinion is that a programmer has seen for a short moment what sysadmins do and decided to make something to help in the task, without really understanding what's needed and what works, what doesn't work, and why.

lmkg 9y ago

If your language is not Turing Complete, then it might be possible to always prove certain properties of programs. Canonically, you might be able to prove that the program will always complete and exit in finite time on any input. Other properties include guaranteeing that an error will not be thrown (or will be thrown), or bounding the amount of time or memory consumed, or guaranteeing that the output of a function will be within a certain numeric range.

tincholio 9y ago

For instance, if you want to make guarantees about program termination (as the author does here). This is not possible for Turing complete languages.

chowells 9y ago

You would always prefer to not have Turing completeness in your language, all other things being equal. Turing completeness isn't ever necessary to write the logic you want to write. But all other things are not equal. There is a cost to giving up Turing completeness. The language must now ensure additional properties about the code, mostly related to termination and productivity. The two strategies for this are reducing functionality offered by the language until you can prove all programs are good and introducing tools into the language to write compiler-verified proofs about your code. Dhall is an example of the former approach. It removes enough pieces that it can only express computations that terminate. Language like Idris, Agda, and Coq are examples of the latter. They provide rich systems that allow you to express proofs of various properties as needed to avoid Turing completeness. Both categories of language are currently difficult to use for general purposes software. Turing completeness is a sacrifice made to ease writing software at the cost of making certain bugs possible. At the moment, the best times to use a non-Turing complete language are when you have a problem domain where you can be satisfied with a reduced power language, or when you want to go all the way in the opposite direction and write machine-checked proofs about your software. As we study these things more, we find ways of easing the burden of using languages that aren't Turing complete. Maybe in the far future, systems will be good enough that most software can comfortably be written in languages that aren't Turing complete. It's a worthy aspiration. It's not now, though.

RodgerTheGreat 9y ago

In layman's terms, it is impossible to determine certain properties of an arbitrary program written in a Turing-complete language. Properties like "will this program finish within a reasonable amount of time?" or "does program X do the same thing as program Y?" For a non-turing-complete language, it may be possible to test such properties. It's crucial to understand that this distinction is not one of how practical it is to determine properties; once you open the door to Turing-completeness, all ability to reason about a program effectively flies out the window. You might be able to come up with rules-of-thumb that determine an interesting property of a program in a Turing-complete language some of the time, but there will always exist programs for which your rules-of-thumb are insufficient.

Gabriel439 9y ago

Here's a practical example of why it's beneficial to not be Turing complete. In Dhall, you can normalize programs, even if they are functions. For example, the interpreter can automatically simplify this Dhall function: let replicate = https://ipfs.io/ipfs/QmQ8w5PLcsNz56dMvRtq54vbuPe9cNnCCUXAQp6xLc6Ccx/Prelude/List/replicate in let exclaim = λ(t : Text) → t ++ "!" in λ(x : Text) → replicate +3 Text (exclaim x) ... to this one: λ(x : Text) → [x ++ "!", x ++ "!", x ++ "!"] ... even though we haven't applied the function to any arguments yet. You can't perform this sort of simplification (in general) if the language is Turing-complete This sort of automatic simplification comes in handy a lot when authoring configuration files. For example, if somebody objects to the import of the remote `replicate` function, you can just simplify the file and (voila!) all the imports are gone because they've all been inlined and reduced. Similarly, if somebody objects to excessive use of abstraction and functions you can similarly simplify them to remove all indirection

skybrian 9y ago
This is inlining a function and unrolling a loop. It's done in many languages, no? More generally, many automatic refactorings are not entirely safe but we do them anyway, assuming that the code will terminate (since intentional infinite loops are rare) and relying on tests and human reviewers to check for mistakes. Depending on the program, substituting equals for equals might have to be rolled back for performance reasons; computing a mathematically equal value is no guarantee.
- Gabriel439 9y ago
  In a Turing complete language you can't safely inline all functions to completion without risking an infinite loop. In such a language there is no decidable way to know when to stop inlining things
  - skybrian 9y ago
    It doesn't matter in practice, because we don't need to inline every function.