It would be difficult to write a C++ program, which can be proven to fulfill all contracts and asserts. (we see with Rust how difficult just proving some types of memory safety are) And there is the halting problem, so some conditions may be impossible to decide either way.   But one could combine contracts and asserts and runtime error or state checking at strategic points. So an interactive compiler/IDE may notify the user, what (boolean) expressions cannot be proven, either by  - providing a contrary case, showing that the program may exhibit an invalid state. Then the user has to fix a bug.  - or just notifying the user that it cannot proof or disproof. Then the user can insert cautionary runtime error checking and also showing  - which expressions in the code do not have to be checked as they can be proven (so which runtime checking can be removed or is removed by the optimizer anyway, so the source code can be simplified)     -----Ursprüngliche Nachricht----- Von:Jonathan Grant via Std-Proposals <std-proposals_at_[hidden]> Gesendet:Fr 22.05.2026 01:14 Betreff:Re: [std-proposals] std::unreachable<T>() An:std-proposals_at_[hidden]; CC:Jonathan Grant <jgrantonline_at_[hidden]>; On 21/05/2026 23:42, Sebastian Wittmeier via Std-Proposals wrote: > 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. That's a good point, would be be useful if vendor compilers outputted proofs from their control flow analysis. Maybe it's visible in the intermediary files. Any code change that causes a constraint failure will clear in the build diagnostic warning/error compile time contracts like compile_assert P4021. This negates the need for C++26 runtime contract assessment - impossible to prove 100% a runtime C++26 contract is satisfied if the compiler's control-flow analysis cannot remove the runtime contract code.. because the C++26 contract is still referenced in the resulting ELF. I put some slides together earlier this year https://github.com/jonnygrant/compile_assert/blob/main/slides/compile_assert_cpp_london_March_2026.pdf Do you think it's more useful for functional safety to be validated at compile time? Regards, Jonathan > >   > >     -----Ursprüngliche Nachricht----- >     *Von:*Alejandro Colomar via Std-Proposals <std-proposals_at_[hidden]> > >     trap;  // diagnosed unless proved unreachable. > >   > > -- Std-Proposals mailing list Std-Proposals_at_[hidden] https://lists.isocpp.org/mailman/listinfo.cgi/std-proposals