is type checking in D undecidable?

[Bruce Carneal]

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.