If I write a program X and tell you it was proven correct, do you know that X is useful?
To know that a correct program is useful, you have to know what it does. And if you know what it does, you have constructed an implementation.
Which is to say that a nonconstructive verifier is really just deferring the 'constructive' part of its operation to the compiler and programmer. (And this is the 'hard part' I was referring to.)
We are discussing the (dis)advantages of HOL vs constructive reasoning (e.g. Coq). The main
difference is that HOL-based provers like Isabelle/HOL has
classical built in from the start -- all proof automation supports classical
reasoning. Constructive reasoning eschews classical methods.
In order to prove the correctness of a program X, I need a
specification S, and then I construct a proof P that X |= S, i.e. that X
satisfies the specification S. I use an interactive proof assistant
to check the proof P. There is no disadvantage that I can
see if the proof P of X |= S is classical, at least from the point of
view of program correctness.
To know that a correct program is useful, you have to know what it does. And if you know what it does, you have constructed an implementation.
Which is to say that a nonconstructive verifier is really just deferring the 'constructive' part of its operation to the compiler and programmer. (And this is the 'hard part' I was referring to.)