We run proofs on code all the time, it's called type-checking.

What you mean is that it's practically infeasible to verify every program behaviour we're interested in. That's probably true for large enough programs, but it doesn't mean we can prove nothing about them.