The language is Turing-complete, not the program. Rice's theorem says that we can't have a program that verifies a non-trivial property for all other programs. It doesn't say we can't verify that property for some programs. That would imply you could never know anything about a program.
> The language is Turing-complete, not the program.
That means we can't make the claim that a particular program, running in that language, is error-free. I don't get why people find this so hard to understand.
> That would imply you could never know anything about a program.
No, it means we can't make the claim that a program is error-free. That's the simplest statement of the Halting Problem.
When someone applies Lean to verify the correctness of a chain of logic, they must remember than Lean cannot be proven to be error-free, because ... wait for it .. Lean is Turing-complete.