It seems like the obvious point of tension is that you probably want AI to be constrained to/by some rigor. Rust is good because it enforces some safety measure

It seems like the obvious point of tension is that you probably want AI to be constrained to/by some rigor. Rust is good because it enforces some safety measures, but I'm more interested yet in the work to have AI work with lean4 or the like to prove its code is up to spec. But that proof checking is probably in direct conflict with fast compilation.