Any language's code can be integrated or transformed into some Turing-complete language. That doesn't make a language powerful. You don't see anyone raving abou

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