Yep 100% agree. And the good news is that we are moving closer every day to having tools that make proving code correct practical. Languages like Idris, Agda, L

Yep 100% agree. And the good news is that we are moving closer every day to having tools that make proving code correct practical. Languages like Idris, Agda, Liquid Haskell, F* (F-star), LEAN etc. are spearheading this movement. If Rust had Refinement Types added it would turn it into a killer language for writing correct high performance code.