| > programming and proving are special cases of a single general activity: constructing a mathematical object. Painting your house and painting the Sistine Chapel are also special cases of a single general activity. Or writing a shopping list vs. a novel. That doesn't mean that the motivations, concerns or skills are similar. > yet nobody would be taken seriously (in the mathematical community) who uses this as an excuse for lowering the standards of proof. Right, they just don't prove much and move on. Again, the motivation is different. In programming the standard isn't even proof. It is bad to spend 10x the cost to ensure zero bugs if the requirements don't call for zero bugs. In the vast majority of formally verified safety-critical software systems, the standard is very high yet proofs are hardly used at all, but rather model-checkers. I am aware of quite a few algorithms proven correct (informally) in prestigious peer-reviewed journal that have later been found incorrect by model-checkers. I am not aware of examples to the converse. Mathematicians don't like model-checking even when completely exhaustive, because their motivation is insight. But for programmers, the motivation is meeting requirements. > Dijkstra anticipated the need to devise program structures that are amenable to formal reasoning. And yet, it is uncertain whether this is generally possible, and empirical evidence suggests that real-world instances are close to the intractable worst-case. Wishing for something doesn't make it so -- at least not yet. BTW, Dijkstra made his more sweeping statements before results about proof complexity were known (initial results in the seventies, and many more in the eighties, nineties and oughts). > Then quantify the bug, and make it a part of the specification. It is, just not part of a formal spec. Specifying and verifying probabilistic properties is especially hard and costly, and as someone who has actually used formal methods for real systems in industry, I know that formal methods are not binary. Like everything else in programming, you must weigh the cost and the benefit of every decision. |