3 ms·
In the context of programming languages, constructive mathematics maps well to type systems. There are type systems that correspond to non constructive logics,
by ufo 5y ago
In the context of programming languages, constructive mathematics maps well to type systems.
There are type systems that correspond to non constructive logics, but those are the weirder ones.
- johncolanduoni 5y agoContemporary type theories have little issue with adding the law of excluded middle as an axiom, though for some intensional type theories it will end up being the only axiom that doesn’t reduce (i.e. have a computational rule associated during simplification) in a useful way. Programming language type systems rarely form consistent logics so there introducing it has no real effect either way.