[credit_guy]

People think mathematics is about proving theorems.

I think that's just an accident of history.

When we write software, we very seldom write proofs that our algorithms are correct. We just write tests, and we also run the algorithms and when they fail we know we have a bug and then we proceed to debug, fix, and add new tests (if we are disciplined, but most of us are). In time, by usage and testing, we gain confidence that our battle tested software is correct, mostly. And we tell people that we will never be 100% confident that any software is bug free. But that's a slight lie: if we wanted such confidence, we would start using provers, and create bug-free software. That possibility exists, but it's just extraordinarily expensive.

Well, in math that's the only possibility, and we use it. And it is indeed extraordinarily expensive, but it's also the cheapest among the alternatives. The alternatives are 2: be rigorous and do these proofs, or be sloppy and allow bugs to creep in, and allow an entire school of math to collapse like the Italian school of algebraic geometry [1].

There is one more alternative. If a particular math theorem has some applicability, then you write a program and use it in real life. In time you eliminate the bugs as much as you can, and you get to the steady state of "virtually bug free". At that point you don't have a solid proof that the theorem is correct, but in general you don't really care. Because you feel that a formal proof is just a thing one would pursue for getting academic satisfaction only.

[1] https://en.wikipedia.org/wiki/Italian_school_of_algebraic_ge...

[dkural]

Your example of the Italian school is well taken, although most of their results were later proven to be correct in the right setting. Severi's example is particularly egregious and I think a major reason this became a thing is Severi's refusal to course-correct and accept that some of the results were not correct. It has echoes of Mochizuki, and I fear, once you dig deeper, some issues around the initial declaration of "We've proven the Classification of Finite Simple Groups". There were many genuine gaps, and a lot of lore taken for granted. The sociology around how this happened is interesting - rushing to announce that it was done was the major mistake, it took away almost all incentive to actually write up the proofs and take them through proper peer-review. Genuine mathematical work was falsely reduced to "write up".

[christina97]

I thought this comment would go in a slightly different direction: the body of work that is mathematics has plenty of “bugs”; proofs with mistakes or other human errors. Yet we take the body to be correct (we believe it “works”) in aggregate, partly because the intuition of mathematicians tells us that these bugs are solvable and don’t bring down the whole. Of course the less intuitive/more surprising/more central the statement, the stricter the standard for proof and more eyes that have walked through it.

[andai]

It's interesting that mathematics, which is mostly recreational (I received profound disdain at the math department for asking about applications!) has such rigorous standards, but software, which entire civilizations now run on, does not.

[radokirov]

It is because you can precisely define what would make the whole mathematical endeavor collapse (not following the rules of logic or showing inconsistency), while even defining precisely what would be undesirable for software requires bringing in the whole physical world. If you can't define the outcome you want, you can't have rigorous standards to follow.

[pclmulqdq]

If a piece of software is in safety-critical applications these days, it is often required to have a proof of correctness.

[andai]

Like Linux? ;)

[pclmulqdq]

I think you might be surprised that Linux is generally not involved in safety-critical systems. There is a whole separate ecosystem for those applications.

[andai]

What do they use for that? BSD?

[pclmulqdq]

The ones that use an OS generally use seL4 these days.

[simiones]

This is a bit reductive about what "proof" actually means in mathematics. Even in math, the kind of formal proofs that tools like Coq can automatically verify are an extreme, and lots of accepted and practiced math is not doing that. Proofs are often more abstract and even occasionally hand-wavy (for example not proving "obvious" statements or minor lemmas).

Mathematicians also occasionally build on top of unproven foundations (e.g. all popular asymmetric encryption schemes are built on top the assumption that certain problems such as integer factoring are hard, for which there is no formal proof), or at least explore both possibilities for statements with unknown truth value (e.g. you can find lots of work that explores the consequences of P = NP and/or P != NP).

However, there is a major separation between math and programs that I think mostly invalidates your proposal - most math we're talking about here is simply not applicable directly to the real world in any way. It's only studied for the interest of mathematicians. There is no real world consequence for Fermat's last theorem, for example - it was just a really interesting to prove theorem. In directly applied math, such as engineering, it is in fact much more common to work with unproven but well tested conjectures.

[RandomLensman]

> In directly applied math, such as engineering, it is in fact much more common to work with unproven but well tested conjectures.

What specific areas were you thinking off? I don't recall, e.g., in numerics that things were often just unproven/conjectures, but might be subject matter specific.

[simiones]

Well, it's not exactly engineering, but physics often uses quite informal math. For a pretty modern example, the Dirac delta "function" was used long before it was formally described; and I have heard it said that even today String theory uses some math that is not fully formalized - though I can't say I know what specifically, so I may be wrong. Newton expressed calculus in terms of inifinitesimals (the dx notation was simply an infinitesimal delta x, not merely notation for derivation), which were not not formalized until much later, after they had already fallen out of favor and had been replaced in formal math by the delta-epsilon limits-based constructions.

Edit: one better example from modern physics - the path integral formulation, used in both string theory and other areas of QM/QFT, is not fully formalized and formally proven to work. Also, a more concrete example of a widely used but actually still unproven conjecture in string theory is the famous AdS/CFT correspondence.

[seanhunter]

Newton didn't use dx/dy. That's Leibniz' notation. Newton's notation for the derivative is just to pot a dot above the letter so ṙ would be Newton's symbol for speed (dr/dt) and two dots would be acceleration (d^2r/dt^2) in Leibniz' notation. Physicists still use Newton's notation but only for derivatives with respect to time these days.

The part of Newton's theory that was troublesome is his fluxions don't have the Archimedian property. It took until the 1960s before Newton's notion of fluxions became rigorously formalized with Non-standard analysis. https://en.wikipedia.org/wiki/Nonstandard_analysis

[simiones]

Oops, I confused some history, thank you for the corrections!

[pfdietz]

Physics famously has a rather cavalier attitude toward formal rigor, but that's because the ultimate test is comparison with experiment. String theory shows what happens when that bulwark against error is missing.

[satvikpendem]

> When we write software, we very seldom write proofs that our algorithms are correct. We just write tests, and we also run the algorithms and when they fail we know we have a bug and then we proceed to debug, fix, and add new tests

But this is due to a "failure" of programming language progress. We've had formal languages for a long time (see Ada and SPARK) and we've simply failed to use them for most scenarios, instead regressing to imperative manually memory managed languages like C and then deriving from that branch.

[dboreham]

One thing I've realized after quite a long life of learning and contemplation is that: mathematics and software are essentially the same thing. Add to that that it might be the case that Physics is the same thing too. We'll see on that one, but there are signs...