[reggieband]

I think it feels easier to say that now that we are long past the point where the debates occurred. But this happened during a time when universities were still trying to figure out how to divide up sciences.

Nowadays, the idea that math has a role to play in pretty much every science isn't really questioned at all. I mean, imagine I suggested that something other than math should be brought to bear on physics. I doubt a single person in here would support such an approach on any level. I think that represents a clear win. Answering objections about the fundamentals of math using formalisms like ZFC was a component of that.

[empath75]

ZFC has very little to do with why math is used in universities or the sciences, and it would still be used even without it, because as you said, it works. It worked for 3000 years before we had ZFC after all.

ZFC wasn’t even the end of the debate on mathematical foundations even in math. There are a lot of people trying to redo everything with types and category theory today.

[reggieband]

ZFC follows along a path including (but not started by) Russell/Whiteheads Principia Mathematica, which famously (infamously?) takes several hundred pages to prove 1+1=2. I doubt very few have thought ZFC (or it's variants) would be the last word.

Almost no scientists cared about formalizing or proving the soundness of the mathematical tools they used. In the same way the majority of programmers do not care about proving the soundness of their programming languages. In general, people seem to be interested in the practical aspects of their work.

But the general idea that symbolic logic is the primary basis for understanding the world is something a bit different and something we rarely question now. I think people assume that this is some obvious thing but it is actually an idea that was coordinated and forwarded. It appears to me that the debate at the beginning of the 20th century around using set theory to establish the foundations of math by way of logic is when the scale seems to have heavily tipped towards that particular idea.

[aratakareigen]

I can't speak for scientists, but programmers usually care very much about the soundness (not in the Curry-Howard sense) of their type systems.

[reggieband]

I disagree and I'm sure we'd only be able to trade anecdotes and no real evidence. However, my experience working in industry for 20+ years is that almost no working programmers pay any attention to such things. For example, when my team recently decided to switch from Javascript to Typescript there was zero consideration about the fundamental soundness of either language. I had the same experience when a team I recently worked with was debating a switch from Java to Kotlin. Nothing approaching the topic of soundness even came up.

I think hacker news can be a bubble since these deeper issues can sometimes appear here. I recall a recent post about a soundness bug found in Rust and it generated quite a lot of discussion. However, I see that as analogous to the intense scrutiny of a small cabal of scientists/philosophers, the Vienna Circle for example, who did take these fundamentals seriously in math/sciences. I just do not believe and have not experienced that sentiment to be prevalent outside of this bubble.