alt Hacker NewsThis is why dependent types work for modelling maths: you don't actually use your proofs as programs. Sure, the formalism would allow you to, but since you don't care about lemmas like "this proof and that proof are _the same_ for certain kinds of 'inputs,'" you don't run into issues with dependent types. If you try using dependent types, lemmas like the above quickly become necessary and also quickly become unprovable.
There are some theories like HoTT where it's convenient to let the same terms act as proofs while still having computational content and sometimes a distinct identity ("proof relevance"). For example a "proof" of isomorphism that might be used to transfer results and constructions across structures, where isomorphisms can be meaningfully distinct. Of course you do retain a significant subset of purely logical arguments where no computational content is ever involved and "identity" becomes irrelevant again.