Skip to main content
Source Link

To widen the angle a bit, I would like to point out that there is a certain analogy between mathematics and software. Programs are formal constructs that are composed and processed according to formal rules, like mathematical proofs. In fact, for particularly "clean" types of software, for example proof checkers based on dependent type theory, programs are proofs, according to the propositions-as-types paradigm. And just like ordinary software is organized in say, classes and modules, mathematics is organized in propositions and even whole libraries of propositions ("topology", "group theory") that are "exported", like modules.

Now, the world has a lot of buggy software. Sometimes this can lead to catastrophe. But catastrophe is remarkably rare. Because, the more heavily the world relies on a piece of software--that is, the greater the "user base"--the more likely will critical bugs be found and fixed. Alternatively, a critical bug might only do harm when the consumer of a module uses that module in an unusual way. (Called "edge case" in software engineering.)

It would not be surprising if a similar effect stabilizes mathematics--the software that runs on our minds.

Post Made Community Wiki by Carsten Führmann