> The only way to define non-computable things is to use excluded middle or choice. There is no other way. At least not in the underlying type theories of proof assistants such as NuPrl, Coq, Agda and Lean.

Meanwhile, ACL2 has the excluded middle and can still prohibit defining non-computable things. It needs termination analysis in order to do so, but these type theories rely on that too. Is the forgoing the excluded middle really gaining you the guarantee of computability?