I really wish I'd been introduced to the constructive idea of proof-of-existence ages ago. It's a really powerful concept
Conversation
if you're not familiar, the idea is that a proof of "∃ x. P(x)" is a pair (x, π) where x is a specific value and π is a proof that P(x) is true
1
4
Replying to
I love how tangible it makes it. I don't think I've ever got my head around the classical approach? Constructive proofs (based on dependent types) just seem to work with my brain… maybe it's just my own lack of experience with maths and proof stuff.