I feel like we're talking past each other somehow but I'll give it one more try. In previous post you quoted the Dhall documentation: > The main benefit of ev

I feel like we're talking past each other somehow but I'll give it one more try. In previous post you quoted the Dhall documentation: > The main benefit of evaluation being finite is not to eliminate long-running programs but to make them significantly less probable. In practice, you will discover that you will rarely author a configuration file that takes a long time to evaluate by accident. This might be practical advice, but it's not theoretically sound. It's drawing a conclusion that wasn't proven. Isn't it kind of weird to write proofs without caring about the result of the proof?