> Idris effectively requires you to write a proof of termination, but you can write the proof for any language
That is the benefit of non-turing complete languages, though. Or, in general, the point of languages with useful type systems.
Writing the proof is not trivial, but languages like Rust or Idris make it simple because they force correctness early in the coding process.
> That is the benefit of non-turing complete languages, though.
That's simply untrue. You can write arbitrary proofs about programs in Turing-complete languages, too. In fact, most formal proofs are of programs written in Turing-complete languages.
> but languages like Rust or Idris make it simple because they force correctness early in the coding process.
Rust doesn't actually let you do that, though. In terms of the expressive power of proof, it is far closer to C than to Idris (in fact, from Idris's vantage point, Rust is almost indistinguishable from C).