| > One of the mistakes, IMO, some proof assistants make in their design philosophy is that since, from the perspective of some formal logics, writing programs and proofs are "the same thing", their[sic] is a corresponding equivalence of the two activities. Don't take this as an endorsement of proof assistants, but programming and proving are special cases of a single general activity: constructing a mathematical object. > Both physicists and mathematicians solve equations, but no one would say that physics is math. The crucial difference is that physicists, unlike mathematicians or programmers, don't create universes of their own. Their job is to explain the behavior of the one that already exists. > Mathematicians manipulate objects that are very regular, and reasoning about them is largely tractable Only because they have made them so. Also, insanely irregular and intractable mathematical objects do exist, yet nobody would be taken seriously (in the mathematical community) who uses this as an excuse for lowering the standards of proof. > while programmers manipulate very irregular and very intractable objects. Only because they have made them so. Dijkstra anticipated the need to devise program structures that are amenable to formal reasoning. > The goal of a programmer is to write a program that meets the requirements, which may include some distribution of acceptable bugs that depends on their severity Then quantify the bug, and make it a part of the specification. > (i.e. a major, but non-catastrophic bug occurring once a month and some minor bugs occurring daily are acceptable) Bugs occur in the program, not in its execution traces. |
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.