I should add that even if you have the technology to prove correctness of program, that doesn't mean it's practical to prove correctness of all behavior of the program. I write real life programs in Agda (which is a dependently typed dialect of Haskell in which you can encode arbitrary proofs in type system) and you rarely prove all intended behavior. For example, recently I was writing a parser, and wanted to prove that for all languages I define, they're not empty languages (so that I don't accidentally construct empty languages by writing something like `between 'z' and 'a'` (silly example as this is easy to prevent)). So you start with basics, proving that the language that only contains empty string is not empty. Then you define what it means to be empty (empty is empty, empty+empty is empty etc...). Then you eventually need to prove L1+L2 is not empty if either L1 is not empty or L2 is not empty. Fine, just give a "witness" to each non-empty language so that we at least know these languages have 1 word in them. Then you have to prove things like "if string in L1 then string in L1+L2". Anyway, long story short, this one extra check I wanted to make, ended up being its own project that took maybe a week. It was definitely -- and I can't stress this enough -- definitely not worth the time.

Being engineers requires you to assess the risk, and if something is not worth checking, there is no reason to check it.