exactly. somehow many people have the idea that C-like imperative code harbours bugs because it cannot be formally reasoned about, and the answer is writing code that can be formally reasoned about.

That the resulting code is many orders of magnitude larger and more complicated than the "informal" original, and often simply cannot exist, and is incomprehensible to most humans if it does, is left as an exercise for the reader.

I mean, formal methods cannot even prove collatz conjecture terminates. Somehow that thing seems to be running some sort of almost turing complete machine in the number encoding. Good luck formalizing existing software!