Only tangentially related to the article, but Agda does allow termination checking to be disabled on individual functions: https://agda.readthedocs.io/en/latest/language/termination-c...