[metafunctor]

Dhall appears to be expressive enough that I can't see why you wouldn't have to refactor and maintain the Dhall code?

Writing Dhall code look exactly like programming to me, and the programmer must possess the necessary programming skills to produce good Dhall code. A random guy with a text editor will make an equal mess in Dhall as they would with a “real” programming language.

I don't see how the restrictions in Dhall really help much in this regard. Turing completeness feels like a red herring to me.

[js8]

Not a user of Dhall, just a fan, but refactoring of Dhall configuration should be extremely easy. You make a change, and your configuration stays the same, which is easy to verify. (Thanks to https://en.wikipedia.org/wiki/Normalization_property_(abstra... )

For TC languages, comparing if two programs (original and refactored) do the same thing is not solvable in general. If the language is not TC then it is more feasible.

[metafunctor]

You can compare the outputs of two programs.

Sure, a TC program may not finish to produce output you can compare, but in my experience that's only a theoretical problem.

[Gabriel439]

You can do more than just compare the output of two programs in Dhall. You can verify using a semantic integrity check that two programs are the same for all possible inputs. For example:

  $ dhall hash <<< 'λ(x : Natural) → x + 0'
  sha256:986613701cf8cc883c2490af81d5fdcfb0f33f840870acaac21689f57c1baab6

  $ dhall hash <<< 'λ(x : Natural) → x'
  sha256:986613701cf8cc883c2490af81d5fdcfb0f33f840870acaac21689f57c1baab6

  $ dhall hash <<< 'λ(y : Natural) → y'
  sha256:986613701cf8cc883c2490af81d5fdcfb0f33f840870acaac21689f57c1baab6

The cryptographic hash is smart enough that many behavior-preserving changes don't perturb the hash.

[js8]

Actually with Dhall, you should be able to compare the programs themselves, even without full "input" (there is even example on the Dhall page, see "You can reduce functions to normal form, even when they haven't been applied to all of their arguments").

So you can for example leave some parameters out of your config and still validate the correctness of refactoring.

If you use general purpose programming language, then even comparing just output might be difficult - most languages allow to do I/O, so it's possible that the configuration is dependent on some side channel.

I would say if you are only using general language "sensibly" for configuration then you are effectively restricting yourself in the same way that Dhall does.

[gdfasfklshg4]

This sounds like a render test?