[Umn44]

The problem with "proofs" is that software is often an iterative process because the environment and problems are constantly changing. If you have a fixed known problem you can do proofs to your hearts content, but in a changing environment you make the most of it with limited resources.

[eru]

You don't have to proof everything. Eg just halting is good enough for a lot of things. (And this is not the general halting problem. Writing programs that provably halt is almost trivial.)