Friday, January 17, 2020

Why Dhall advertises the absence of Turing-completeness

total2

Several people have asked why I make a big deal out of the Dhall configuration language being “total” (i.e. not Turing-complete) and this post will summarize the two main reasons:

  1. If Dhall is total, that implies that the language got several other things correct

  2. “Not Turing-complete” is a signaling mechanism that appeals to Dhall’s target audience

“Because of the Implication”

The absence of Turing completeness per se does not provide many safety guarantees. Many people have correctly noted that you can craft compact Dhall functions that can take longer than the age of the universe to evaluate. I even provide a convenient implementation of the Ackermann function in Dhall to make it as easy as possible for people to foil the interpreter:

However, a total language like Dhall needs to get several other things correct in order to be able to guarantee that the language is not Turing complete. There are multiple ways you can eliminate Turing-completeness from a language, but nearly all of them improve the language in some way.

For example, the way Dhall eliminates Turing-completeness is:

  • Eliminating general recursion

    … which protects against common mistakes that introduce infinite loops

  • Having a strong type system

    … especially one with no escape hatches for reintroducing general recursion

  • Forbidding arbitrary side effects

    … which can also be another way to backdoor general recursion into a language

These three features are widely viewed as good things in their own right by people who care about language security, regardless of whether they are employed in service of eliminating Turing-completeness.

In other words, Turing-completeness functions as a convenient “umbrella” or “shorthand” for other safety features that LangSec advocates promote.

Shibboleth

According to Wikipedia a shibboleth is:

… a custom or tradition, usually a choice of phrasing or even a single word that distinguishes one group of people from another. Shibboleths have been used throughout history in many societies as passwords, simple ways of self-identification, signaling loyalty and affinity, maintaining traditional segregation, or protecting from real or perceived threats.

The phrase “not Turing-complete” is one such shibboleth. People who oppose the use of general-purpose programming languages for configuration files use this phrase as a signaling mechanism. This choice of words communicates to like-minded people that they share the same values as the Dhall community and agree on the right balance between configuration files being data vs. being programs.

If you follow online arguments about programmable configuration files, the discussion almost invariably follows this pattern:

  • Person A: “Configuration files should be inert so that they are easier to understand and manipulate”
  • Person B: “Software enginering practices like types and DRY can prevent config-induced production outages. Configs should be written in a general-purpose programming language.”
  • Person A: “But configuration files should not be Turing-complete!”

Usually, what “Person A” actually meant to say was something like:

  • configuration files should not permit arbitrary side effects
  • configuration files should not enable excessive indirection or obfuscation
  • configuration files should not crash or throw exceptions

… and none of those desires necessarily imply the absence of Turing-completeness!

However, for historical reasons all of the “Person A”s of the world rallied behind the absence of Turing-completeness as their banner. When I advertise that Dhall is not Turing-complete I’m signaling to them that they “belong here” with the rest of the Dhall community.

Conclusion

In my view, those two points make the strongest case for not being Turing complete. However, if you think I missed an important point just let me know.

2 comments:

  1. Doesn't the absence of Turing-completeness also make static analysis easier?

    ReplyDelete
    Replies
    1. Any static analysis that depends on the absence of Turing-completeness can still choke on pathological expressions like the Ackermann function. However, if you eliminate general recursion then that tends to imply that you are less likely to write such pathological functions by accident. So you might say that it at least makes it less likely that the user unintentionally overloads such static analysis.

      Delete