> Thankfully, this sort of analysis tends to use "constructive logic"; in which case, we're told why some property isn't provable (either because we're given a counterexample proving it's incorrect, or we're told which assumptions/preconditions need to be proved first)
That's not what constructive logic means.