On Monday, 6 June 2022 at 04:59:05 UTC, Ola Fosheim Grøstad wrote:
An assert only says that the logic of that particular function
is not meeting the SPEC.
Actually, the proper semantics are weaker than that, the spec
would be preconditions and post conditions. Asserts are actually
just steps to guide a solver to find a proof faster (or at all)
for that particular function.
In practice asserts are «checked comments» about what the
programmer assumed when he/she implemented the algorithm of that
function.
A failed assert just says that the assumption was wrong.
If the compiler can prove that an assert holds given legal input,
then it will be removed. As such, it follows that asserts has
nothing to do with undefined behaviour in terms of illegal input.
The assert is not there to guard against it so the compiler
removed it as it assumes that the type constraints of the input
holds.
