4 ms·
Intuitionism has had a great impact on computer science and the design of many programming languages. It's now widely known that an intuitionistic proof has co
by nextaccountic 3y ago
Intuitionism has had a great impact on computer science and the design of many programming languages.
It's now widely known that an intuitionistic proof has computational content (through the curry-howard correspondence)
Those things have a real world impact
- theamk 3y agoI have no doubt it had an impact on Curry personally, but it does not it has direct impact to on the the computer science. The Curry–Howard correspondence is formulated entirely in mathematical terms, and no philosophy is required to understand and use it. For example, Robert Goddard, who invented first liquid-fueled rocket, became interested in space when he read Wells' "The War of the Worlds". So did Wells' work had an impact on rocket science? Certainly. Does it mean you should read "The War of the Worlds" if you want to build rockets? Probably not.
- nextaccountic 3y agoThe philosophy has an impact in the mental model and the learnability of the mathematical theories. Technically you could learn and use the mathematics without knowing the philosophy behind it but in practice almost nobody does that. It's like knowing design patterns in OO: it's ultimately all software right? But software exists first in the mind of the programmer, and what's written in the IDE is just a shadow of what the programmer imagined. This makes one appreciate the point that there are things in software that exists entirely inside our heads