The thing is that proving small functions to be correct is often quite useless. You can cover them well enough with a set of unit tests. The big challenge are l

The thing is that proving small functions to be correct is often quite useless. You can cover them well enough with a set of unit tests. The big challenge are larger parts of the code, like entire classes or parts of a program. These kinds of things are very hard to prove formally. Even if you did prove them formally, the spec according to which you programmed might be wrong, or the compiler might be wrong (I've seen a variety of compiler bugs, especially larger projects uncover them). Formally proving code is like making sure that every single screw of a self-driving car is tightened to an exact torque, but then the car runs over a person anyway. It's solving the wrong problem.