3 ms·
I'm not familiar with any curriculum focusing on constructivist foundations. Out of curiosity, why do you feel constructivist foundations would be more compleme
by throwawaymath 7y ago
I'm not familiar with any curriculum focusing on constructivist foundations. Out of curiosity, why do you feel constructivist foundations would be more complementary to theoretical computer science?
- logicchains 7y agoConstructive maths is generally computable maths, which means less worry about whether whatever you just did is computable or not.
- Gondolin 7y agoMore precisely the effective topos is a kind of realizability topos with a nno where every function is computable. Such a (non trivial) topos cannot be classical, otherwise the halting problem would be decidable. However the effective topos can only deal with calculability, not complexity. For complexity linear logic (without exponentials) and symmetric monoidal categories are better suited (but I don't know if there exists a model where every function is in P for instance).