Could you elaborate or illustrate what you mean by "theorem proving systems that embrace the full spectrum of abstract and correct thought"?

As a mathematician (and programmer on the side) who regularly works in Coq, my impression is that Rust does represent "the future of programming" (or rather, my ideal of it). Type systems are the only mechanism (that I know of) for formally ensuring properties of programs, and proof assistants and languages like Rust lie on two extremes of the spectrum. The former puts the type system in focus; indeed all my work in Coq is about convincing the compiler that certain functions (terms) type-check. The latter puts types in the background, trying to prove as much as possible with minimal friction.

What's the alternative?