You probably have no experience with constructive proof checkers, else you wouldn't be missing Auggie's point. > I'm sure they would much prefer that it was co

You probably have no experience with constructive proof checkers, else you wouldn't be missing Auggie's point. > I'm sure they would much prefer that it was constructive, rather than non-constructive One point against constructivism is that the proof could be less readable. > can produce a usable algorithm from the constructive proof No. Between the automated tactics and inductive propositions constructed to carry all kinds of redundant state helpful in proving your properties, your proof objects won't be anywhere near production level. And constructive proof checkers don't intend that to happen anyway: you pretty much define an efficient function in a DSL, then use a different DSL to prove that the function fulfils the properties. The proof object is pretty much a black box with unclear efficiency that wasn't meant for humans to read.