[hobofan]

> I, personally, think that it is ridiculous that ~none of the software we use is known to work correctly. It just happens to work correctly, most of the time.

I don't know. It seems to match the general futility of pedantry that exists in all professions. Yes, you can try to optimize for absolute 0 flaws in your code, but in a world where a CPU itself may have bugs in the way it executes assembly, that seems a bit silly beyond a certain point.

[thomasahle]

> in a world where a CPU itself may have bugs in the way it executes assembly, that seems a bit silly beyond a certain point

CPUs are tested so so much more thoroughly than any software today. Including using formal proofs.

If the chance of a CPU bug is something like 1/10^6 and each module in your software is 1/10, reducing that to 1/100 makes a bog difference.

[hobofan]

> software is 1/10, reducing that to 1/100 makes a bog difference

I fully agree! I'm all for moving the needle towards moving the needle towards more formal verification, but what GP is suggesting is full verification of programs, which is more akin to trying to achieve a 1/10^6 bug rate.