4 ms·
Using formal methods, the only place where you have near-perfect assurance of no bugs is between the spec and the code. You can't have a bug-free spec without
by dkarl 16y ago
Using formal methods, the only place where you have near-perfect assurance of no bugs is between the spec and the code. You can't have a bug-free spec without bug-free requirements gathering and bug-free documentation. You can't have those without bug-free natural language communication. Also, a reasonable spec for a complicated piece of software is itself a complicated piece of code. If you can prove the spec is accurate by checking it against a smaller spec, and that spec against a smaller one, until you've reduced a problem of arbitrary size (say, the Eclipse project?) down to a reasonably human-checkable spec, then you run into complexity barriers. How is it possible to rigorously specify something as complex as Chrome or Microsoft Excel in a spec compact enough that you can certify it is error-free?
- ctdonath 16y agoHow is it possible to index the entire Internet's content, and perform nontrivial searches fast enough that a page of hits can be rendered as the searcher types? That may work on a small scale, but scaling up you run into complexity barriers. It's impossible in practice. Oh, right, Google did it. Your reasoning is exactly what the article criticizes: the notion of "that's impossible, don't bother" vs. "so what, let's do it anyway". Our ability to handle complexity scales exponentially over time, and we're on a fast-rising part of the curve now; even if something is "impossible in practice" now, get started on the problem and predict at what point the industry _will_ have the technology to handle that level of complexity. Hard != impossible. Hard now != hard in the relevant future.