Too much a generalization for my taste but in general you’re not wrong: we’re gonna replace easy-ish correctable programmer bugs with somewhat harder to spot theorem [proving] bugs. 
This is why I am not very fond of the more formal and super strict languages like Coq / Idris / Agda et. al. They sound really good in theory but in practice, most programmers are not mathematicians (though it’s not a bad idea for all of us to be, if you ask me, but we all know it’s not happening en masse for sure).
Languages like Rust and OCaml (likely Haskell as well but I am not familiar with it) are doing just fine and IMO they are striking a golden middle.
