[symbolicAGI]

Proving program correctness is not easy. For example, one must prove the correctness of the entire dependency supply chain that the target program might directly or indirectly call. Sure, the proofs of those dependencies are to a degree reusable, but would likely need to be re-proved for each distinct set of parameters.

And on the other hand, TDD shows that having expectations of the results before coding the procedure is a good thing. Not necessarily proving the implementation correct but TDD is more likely to produce correct code.

[jsmith45]

Yeah, proving correct is not a panacea. If you have C code that has been proven correct with respect to what the C Standard mandates (and some specific values of implementation defined limits), that is all well and good.

But where is the proof that your compiler will compile the code correctly with respect to the C standard and your target instruction set specification? How about the proof of correctness of your C library with respect to both of those, and the documented requirements of your kernel? Where is the proof that the kernel handles all programs that meet it documented requirements correctly?

Not to point too fine a point on it, but: where is the proof that your processor actually implements the ISA correctly (either as documented, or as intended, given that typos in the ISA documentation are that THAT rare)? This is very serious question! There have been a bunch of times that processors have failed to implement the ISA spec is very bad and noticeable ways. RDRAND has been found to be badly broken many times now. There was the Intel Skylake/Kaby Lake Hyper-Threading Bug that needed microcode fixes. And these are just some of the issues that got publicized well enough that I noticed them. Probably many others that I never even heard about.