C/C++ has too much undefined behavior. Ada died off. The scripting languages don't need it as much. Rust had potential for proof work, but went off in a different direction. There are modern proof systems, but they're rarely integrated with the programming language.
On the verification side, it's never had more users that I'm aware of. SPARK and Frama-C are very active compared to almost non-existent use of formal methods in industry decades ago. Rust could similarly have a subset integrated with Why3 platform to make the formal methods easier to use. Further, I've seen extraction done from Coq to C and Rust. There's also one person modeling C in WhyML to write the algorithms in the latter but extract to former. Or something like that. Could be done for Rust, too.
Which direction is that?
For some reason, the moment you bring up mathematical thinking, most programmers shy away and claim that this isn't something they should work with 'everyday'.
I never studied CS and I deeply regret that now. I want to up my game and I don't want to always just patch stuff around to infinity, but I honestly have no idea where to start.
What's so wrong with functional languages? I am sure you have heard this cliche a lot but here it comes once more -- I became a much better programmer once I learned an FP language.
Still, back in my Java days I achieved this with a ton of defensive coding, always doing deep cloning before passing complex data structures to anywhere, and trying to enforce design by contract (interfaces and their implementation classes)... which are practically the patterns that any average FP language uses: pattern-matching, immutability and always copying data and thus never passing stuff by reference (always by value), and behaviours / protocols / macros (of the manipulating the AST kind, not in the way C does it).
So to be fair, you are bound to land at an FP language eventually. Maybe you just don't know it yet. Which is fine, learning is about the journey and not the destination anyway.
http://infohost.nmt.edu/~al/cseet-paper.html
https://pdfs.semanticscholar.org/12d5/23e586ffde5cbe020cb3fa...
(Second link has a table and description showing the results they got. Stavely's book distills it into lightweight, less-processy form.)
Design by Contract itself is like assertions on steroids. If your language lacks support, you can build it into your functions at beginning, middle and end. If OOP language, you might use constructors and destructors. If trying to understand it, I have a link that you can give even to project managers.
https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b...
One benefit of making it a formal spec is you can generate tests directly from your specs. This is an old, old technique being rediscovered recently. Various names include specification-based, model-based, contract-based, and property-based test generation. The last thing you can do is manually or automatically convert your specs into runtime checks for the above and/or fuzz testing. The failure takes you exactly to the property that failed if it was one of them.
Finally, for just the most critical things, you can try formal proof on them. SPARK Ada is a great example used in industry with the book being pretty easy to follow.
https://www.amazon.com/Building-High-Integrity-Applications-...
The nice thing about that toolset, esp the proprietary version, is that you can use automated provers to avoid having to do mathematical proof by hand. If something doesn't pass, you have several options: do some manual work on hints to the automated provers or actual proofs in a proof assistant; monkey around with the code to see if different structure or algorithm gets it through; put in runtime checks for just the properties you couldn't prove. If you do the last one and keep programming while solvers run, then the productivity is similar to Design-by-Contract with the extra benefit some properties might hold in all cases. You might also get performance boost by reducing unnecessary, safety checks via proofs that were successful.