Add “ackermann 10 10” to your configuration file and you have something that’s technically proven to terminate, but won’t do so before the sun burns out. No security properties are gained here.
Re:Surprisingly Turing-Complete
by naasking on Sunday April 12, 2020 @10:45AM
(#22848564)
The security property gained is that with terminatation, other sorts of analyses that check security properties of interest now become possible to prove. It doesn't mean they'll be tractable, but "possible" is a necessary precondition for tractable.
And just to be clear, Dhall, the configuration language we’re talking about, is not TC, but powerful enough to compute the Ackermann function: https://gist.github.com/Gabriel439/77f715350ecc0443eed5fa613...
Add “ackermann 10 10” to your configuration file and you have something that’s technically proven to terminate, but won’t do so before the sun burns out. No security properties are gained here.