On Friday, 23 October 2020 at 16:56:46 UTC, Kagamin wrote:
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?
Not my area but after a quick wiki skim my guess is that the
termination checkers would not be helpful at all.
If you do pick up one of the termination checker languages and
experiment, please post back with the results.
