[bigbillheck]

> Ultimately this crowd wants to change the practice of mathematics in the real world, so they are very accomiadating

PhD mathematician in industry here. The way I see it, foundations is to the rest of mathematics the way music theory is to music: it needs to be a describer, not a prescriber. (If I were less charitable I'd have said "ornithology is to birds").

> the mainstream formalizations have clearly failed in that mathematicians that aren't logicians or set theorists would rather engage with them as little as possible

On the contrary, ZFC has been a tremendous success in that most mathematicians don't need to worry about it at all.

[throwaway81523]

Imho, software people should study foundations (particularly proof theory) much more than they do. That is how you ensure correct code, after all. The people deeply involved in software verification are basically logicians. Also, the test suite for the HOL Light proof assistant (used in software verification) uses a large cardinal axiom, sort of. It uses a version of itself with the large cardinal added, to prove the consistency of the normal version without the large cardinal. Neither version can prove itself consistent, because of Gödel's theorem, but the one with the large cardinal can prove the consistency of the one without it.

One can say that if either is inconsistent then they can prove everything, but that makes it even sharper: the large cardinal is used purely to give engineering assurance of software correctness and not real mathematical rigor. So it's a pure engineering use of one of the most "out there" mathematical objects. It doesn't seem worse than using IEEE floating point arithmetic to design airplanes....

[Ericson2314]

> PhD mathematician in industry here. The way I see it, foundations is to the rest of mathematics the way music theory is to music: it needs to be a describer, not a prescriber. (If I were less charitable I'd have said "ornithology is to birds").

That sounds nice, but breaks down when one thinks harder. Music is a little bit physical phenomena, a little more biological phenomena, and even more cultural phenomina. That's many layers at once, and theory has to conform to the evidence.

Math, is not science. This is no evidence external to reasoning. Different foundations / formal systems conclude different things.

At best, we can look at what matches existing working mathematicians mental heuristics and.....that's not ZFC, which admits all sorts of crap because it is untyped.

> On the contrary, ZFC has been a tremendous success in that most mathematicians don't need to worry about it at all.

That is how most mathematicians see it, but us in the type theory crowd see that as bad goalposts necessitated by the fact that ZFC is so clunky to work with --- of course one wants to declare mission accomplished and move on to other things as quickly as possible with a foundation like that.

Check out https://xenaproject.wordpress.com/ for a less heterodox approach, that nevertheless does use a type theoretical "user interface" and "kernel" (trusted foundation) for purely practical reasons. Basically, the idea is making making formalized mathematics not a huge burden necessitates a more ergonomic system than was needed 80 years ago without computers.