That would make the diagnosis dependent on the quality of the "prove engine", of the compiler or static checker settings, possibly of half-unrelated parts of the program (e.g. one indirection more).

Just saying. That all could be okay and reminds of automatic checking for C++ contracts.

One approach could be that a tool that first proves some "fact" creates some machine-only- or also user-readable marking how the proof was done. So other systems can revisit the proof, even if they are less sophisticated. That would give more reliability and stability. And it would also give (more) suitable error messages, if the proof is not viable anymore after a change in the code.

-----Ursprüngliche Nachricht-----
Von: Alejandro Colomar via Std-Proposals <std-proposals@lists.isocpp.org>

trap;  // diagnosed unless proved unreachable.