[ebingdom]

> 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.

[chriswarbo]

The last part about preconditions/assumptions isn't specific to constructive logic; it's about backwards-chaining proof tactics; for example, applying the `ring` tactic in Coq will tell us to prove that the given structure is a ring (see the Errors section of https://coq.inria.fr/refman/addendum/ring.html#concrete-usag... )

The reason constructive logic is nice for this is the first part: we'll be given a counterexample, or a total algorithm for generating counterexamples, etc. (depending on the nature of the statement and its quantifiers). This is preferable to classical logics, where an automated prover might tell us "false", but we have no idea why.

[eperdew]

Yes - to elaborate, a constructive logic is a logic without P or not P. This doesn't have much to do with whether a tool can tell you what obligations you haven't proven. The separation logic based provers I've used have all had excluded middle.