12 ms·
You sure can prove that any correct code does something correct, but you can never prove something about a program outside of a machine-checked formal proof.
by cmrx64 11y ago
You sure can prove that any correct code does something correct, but you can never prove something about a program outside of a machine-checked formal proof.
- nly 11y agoThe problem is that it's far more difficult to prove what code doesn't do than what it does. I can write a function to do X, Y and Z, and I can show, through observation and aggressive testing, that it does indeed do X,Y and Z....but its a lot harder to prove that it only does X,Y and Z and nothing else. Memory safety is just one expression of this problem.
- cmrx64 11y agoIn the typical framework (refinement), if you prove your function does X, Y, and Z, then it does exactly X, Y, and Z. Please don't take my comment out of the context of formal, machine-checked proofs. It is hard, and that's my point.