personally, I will generally just want to construct some artifact which has some property, e.g. the proof is a program to construct something. Where a classica

personally, I will generally just want to construct some artifact which has some property, e.g. the proof is a program to construct something. Where a classical proof doesn't give you this program, it merely states that such a property holds. Which is perfectly fine if that is what you want to know.