Comment by satvikpendem

> When we write software, we very seldom write proofs that our algorithms are correct. We just write tests, and we also run the algorithms and when they fail we know we have a bug and then we proceed to debug, fix, and add new tests

But this is due to a "failure" of programming language progress. We've had formal languages for a long time (see Ada and SPARK) and we've simply failed to use them for most scenarios, instead regressing to imperative manually memory managed languages like C and then deriving from that branch.