Hacker News new | ask | show | jobs
by metafunctor 2690 days ago
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.
2 comments
Gabriel439 2690 days ago
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.
link
js8 2690 days ago
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.

link