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 id

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.