> 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).