3 ms·
Propositions as Types: Explained (and Debunked)
- 082349872349872 3y agoI believe the reason mathematicians generally like classical logics and informaticians generally like intuitionist logics is that mathematicians are already working at the semantic level, and are solely concerned with being, while informaticians are passing between syntax and semantics, and are concerned also with becoming. In the former world, equality is easy, and excluded middle applies; in the latter world, things which are not syntactically equal may later evaluate to be semantically equal, which destroys excluded middle. Similarly, all proofs are equal in the world where we've already forgotten every detail but their existence and all is static, but they are most definitely unequal in the dynamic world in which we're trying to create new detailed paths by welding together the details of paths we already have.