Quote:
Originally Posted by pdurrant
Ah — but only if you get the coding right. It's a lot easier to do a written proof for this puzzle than to prove that a program does what you think it does...  |
You would need to get complete coverage of the data, which you'd need to prove you'd done....
Also, for some problems (less so for this one), complete coverage may not be practically computable. And for some problems a single "run" may not be computationally tractable (is that the right term? I mean that the algorithms that don't have a polynomial time solution). Unless you are the NSA or some such
From memory, there was a silicon design case, an FPU I think -- the details are hazy in my aged mind -- where most of the design was based on formal proofs, apart from one small step handled by a little bit of code... Guess what? The code was wrong and the result was a bug in the design...
Though, to be fair, such approaches can be handy for a quick test to try and verify or disprove a hypothesis. (I have some memory of this also being used, when combined with statistics and distributions to give a confidence value on an otherwise unproven hypothesis, but I can't remember the details.)