It’s embedded in a Turing complete language, but you can’t prove theorems about programs written in a Turing-complete language (Rice’s Theorem) so the ACL2 language itself has to be limited to programs that can be determined to halt. The J-Bob language from the book The Little Prover might be a better example.

There’s a whole programming paradigm here of languages that aren’t Turing complete: https://en.m.wikipedia.org/wiki/Total_functional_programming