[pron]

I'm not at all sure mathematicians would make better programmers. 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 is a corresponding equivalence of the two activities. This is somewhat analogous to concluding that since both programming and writing involve entering words into a text editor, the two are the same. But the fact that, from some specific perspective, both mathematicians and programmers write proofs does not mean that the activities are similar. Both physicists and mathematicians solve equations, but no one would say that physics is math. Mathematicians manipulate objects that are very different from those that programmers manipulate. Mathematicians manipulate objects that are very regular, and reasoning about them is largely tractable, while programmers manipulate very irregular and very intractable objects. Ostensibly, the difference is only in measure, but a difference in any robust complexity measure is usually a difference in quality. Even the actual proofs are very different. Mathematical proofs are usually short but mathematically deep, while program proofs are mathematically shallow and uninteresting, but very, very long and full of detail. Not to mention that the motivations are completely different. 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 (i.e. a major, but non-catastrophic bug occurring once a month and some minor bugs occurring daily are acceptable), and increasing the cost of programming by an order of magnitude in order to make all bugs provably absent is the wrong thing to do. In math, the requirements are completely different.

[catnaroek]

> 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.

[pron]

> 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.