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.
My work is related to homotopy type theory. There are mathematicians working in Agda and Lean (2, but also 3) as well, but it certainly is a niche field.
Ah, makes sense. By being able to express "abstract and correct thought" I mean being able to express myself in a system much like a mathematician would. Coq for example is too constructively oriented for my taste to make that possible (I know, you can "just add an axiom" ...), and its automation is also (therefore?) not good enough.
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?