3 ms·
The 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 ob
by nly 11y ago
The 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.