On Thursday, 22 October 2020 at 18:24:47 UTC, Bruce Carneal wrote:
Per the wiki on termination analysis some languages with dependent types (Agda, Coq) have built-in termination checkers.
What they do with code that does, say, a hash preimage attack?