Having worked on program verification in the past, Rust looks like the most useful modern language to which formal methods can be applied. Rust's rules eliminate so many of the cases that are hard to formalize.
Big remaining problems involve deadlock analysis, both in the thread sense and in the Rc/borrow sense. Those are somewhat equivalent. I'd like to have static deadlock analysis in Rust. If you had that, I think you could get safe back-pointers, too. If you can prove that all borrow and upgrade calls can't fail, you can eliminate most reference counts. That gives you free interior mutability when that's possible.
The author's comment on provers is interesting. The big problem with theorem provers is that they're developed by people who like to prove theorems. They're in love with the formalism. This leads to a UI disconnect with programmers.
You can knock off most things you have to prove with a SAT solver. But you'll need something heavier for the hard problems. Coq is too manual. The author thinks ACL2 is too functional. Not sure what to do there, but I've been out of this for decades.
Machine learning may help in guiding theorem provers. Most programs aren't that original in terms of control flow and data usage. So inferring a proof plan from other code may work. ML systems can't be trusted to do the proof, but may take over guiding the process.