Indeed, and if they want to make these claims why aren't they applying the same logic to Coq, Agda and Idris? These languages are often lauded (correctly) for

Indeed, and if they want to make these claims why aren't they applying the same logic to Coq, Agda and Idris? These languages are often lauded (correctly) for giving up Turing completeness in exchange for improved static safety. But they all can implement rule 110.