I'm not sure I agree. For example CakeML [1] is the first fully verified self-hosting compiler for a substantial programming language, and seL4 [2] is the first fully verified substantial operating system kernel. Both were verified in LCF provers using HOL as a logic. Are you saying that the guarantees of correctness are not in themselves useful?
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.
