They probably should've started with a Wirth-style language plus Design-by-Contract and static analysis. That would knock out tons of stuff at compile and runtime. If looking for mature language, the best one for predictability is SPARK Ada hands down. It was designed for easy analysis in automated provers. It's automation level is a lot higher than it used to be. Folks wanting provable programs should either be considering using it or prototyping their programs in it with semantics-preserving translation to the blockchain language/VM.

https://en.wikipedia.org/wiki/SPARK_(programming_language)

https://www.amazon.com/Building-High-Integrity-Applications-...

Note: The book is designed for people without formal methods background. I can't say how easy or not it will be since I just got it. :)

Are we there yet? 20 Years of Industrial Theorem Proving with SPARK

https://proteancode.com/keynote.pdf

IRONSIDES DNS illustrates it can handle bigger problems

http://ironsides.martincarlisle.com

Frama-C and SPARK both build on Why3 platform with its intermediate language WhyML. Work built on any of these three can usually be ported to the others. So, I'll drop a recent example in Frama-C that's really math heavy with a style amenable to high automation.

https://hal.archives-ouvertes.fr/hal-01681134/document