3 ms·

you can prove theoretical programs. do you really want to have to prove that it still works with any random bit flipped at runtime? what about two random flip

you can prove theoretical programs. do you really want to have to prove that it still works with any random bit flipped at runtime? what about two random flipped bits?

wtallis 15y ago
All proofs start from some assumptions. When you are proving programs, you assume that the hardware is functioning properly. After all, anyone going to the expense of proving their software is correct will also pay for ECC throughout their hardware. Once you've proven your software correct, you can make assurances about the behavior of the software when run on particular hardware, and those assurances will be limited primarily by the reliability of the hardware.
- blackhole 15y ago
  Assuming that hardware will work correctly can be an extremely dangerous assumption.
oconnore 15y ago
What is your point, exactly? Do you think testing (likely on a different machine than the target) will catch a 1 in a million hardware error either?
baddox 15y ago
You're challenging what it means for something to be a proof, which I think is always subject to philosophical debate. Intuitively, something is a proof of a proposition if it convinces someone else that the proposition is true, and the proposition actually is true. Obviously, for difficult concepts, it's possible that every expert in the world could be convinced that a proposed proof is correct, only to later find out that it's not. The way I see it, you're always only proving that something has a high probability of being correct, and showing how high the probability is. For computer software, you might be showing that your program is correct with the same probability that the underlying hardware is working as specified (so cosmic rays shifting bits or faulty hardware are possible exceptions baked into your proof). To get a bit silly, a mathematical proof delivered from person A to person B is really only showing that a proposition is true with the same probability that person B is sane, educated, and is understanding the concepts correctly,

you can prove theoretical programs. do you really want to have to prove that it still works with any random bit flipped at runtime? what about two random flipped bits?

wtallis 15y ago

All proofs start from some assumptions. When you are proving programs, you assume that the hardware is functioning properly. After all, anyone going to the expense of proving their software is correct will also pay for ECC throughout their hardware. Once you've proven your software correct, you can make assurances about the behavior of the software when run on particular hardware, and those assurances will be limited primarily by the reliability of the hardware.

blackhole 15y ago
Assuming that hardware will work correctly can be an extremely dangerous assumption.

oconnore 15y ago

What is your point, exactly? Do you think testing (likely on a different machine than the target) will catch a 1 in a million hardware error either?

baddox 15y ago

You're challenging what it means for something to be a proof, which I think is always subject to philosophical debate. Intuitively, something is a proof of a proposition if it convinces someone else that the proposition is true, and the proposition actually is true. Obviously, for difficult concepts, it's possible that every expert in the world could be convinced that a proposed proof is correct, only to later find out that it's not. The way I see it, you're always only proving that something has a high probability of being correct, and showing how high the probability is. For computer software, you might be showing that your program is correct with the same probability that the underlying hardware is working as specified (so cosmic rays shifting bits or faulty hardware are possible exceptions baked into your proof). To get a bit silly, a mathematical proof delivered from person A to person B is really only showing that a proposition is true with the same probability that person B is sane, educated, and is understanding the concepts correctly,