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?