Any language&#x27;s code can be integrated or transformed into some Turing-complete language. That doesn&#x27;t make a language powerful. You don&#x27;t see anyone raving about how amazing the language of variable-free arithmetic expressions is, but that&#x27;s <i>already</i> integrated into most languages people would call &quot;powerful.&quot;<p>The idea that ACL2 verifies a powerful language is outright false. ACL2&#x27;s verified language is stripped down (no first-class functions, nontermination, exceptions, etc.) <i>because</i> added power makes it too hard to verify.