3 ms·
the tricky bit is that pen and paper proofs break down when managing software level of complexity of that sort, and mechanized theorem proving is tough even wit
by carterschonwald 18y ago
the tricky bit is that pen and paper proofs break down when managing software level of complexity of that sort, and mechanized theorem proving is tough even with toy examples
- dinkumthinkum 18y agoI don't think he's talking about a formal mathematical proof, rather inspecting the code and understanding it thoroughly such that you can show, without the Pumping Lemma or anything like that, that memory access is being done properly.
- nostrademons 18y ago...which is also exceptionally difficult. Yeah, there're tricks you can use to make it easier, like RAII and thoroughly documenting ownership of parameters. But once you get past a few tens of thousands of lines, written by more than one programmer, it becomes essentially impossible to understand it thoroughly enough that you can tell by inspection whether it'll leak memory.