assert the Compiler Does Not Prove Is Refused, Unless the Build Says warnStatus: Accepted
Date: October 23, 2026
Answers: what the compiler does with an assert it cannot prove
Amends: ADR-269 D4 (no build option chooses between the
two)
Related: ADR-269 D5, D7, D8 (preconditions, --asserts,
refuted-claims), ADR-360 D3 (main’s preconditions),
ADR-369 (a struct’s rule), ADR-376 (assume)
assert(cond) is a contract: the compiler proves it while the program is
built, and where it cannot, it checks it when the program runs
(ADR-269 D4). Until now the second case was silent. A program whose claims
were all proved and one whose claims were all checked at run time built the
same way, with the same output, and only --asserts told them apart.
That makes the language’s claim of verification hollow where it matters: a
reader who sees assert cannot tell whether it was proved, and a build that
passes says nothing about it. A language that offers proofs has to say, by
default, when it has none.
Other languages: Dafny, SPARK and F* refuse a program whose verification
conditions are not discharged, and offer an explicit way out ({:verify
false}, pragma Assertion_Policy, admit). Rust’s and C’s assert! are run
time checks only and claim nothing more.
assert not proved is refused, NK1300.An assert the compiler does not prove refuses the program, NK1300:
The message says that not proved is not false: the compiler could not show
the claim from what it knows where it stands. It names why, as --asserts
does.
Not asked: a precondition of main, which is checked where the words arrive
(ADR-360 D3), as a guard for data from outside the program; a claim in a
test, the test’s verdict; an assume, which the program vouches for
(ADR-376); a claim about data from outside the program, refused already
(NK1202). An index or an overflow the compiler does not prove is not a
claim the program wrote: it keeps its check, as the language promises
(Part I 2.2).
unproved-claims = "warn" builds it, the claim checked.[build] unproved-claims is error, the default, or warn;
--unproved-claims overrides it for a single build. At warn each NK1300
is a warning, and the claim is checked where it is reached and stops the
program when it is false, as every build did before this record. The choice
is part of the build’s cache key, as refuted-claims is (ADR-269 D8). The
check sees no switch: it reports every claim it did not prove, and the build
decides the severity.
A program does not have to rewrite a claim as a guard to build at warn: the
compiler emits the check.
error on request. A program would still build
with claims nobody proved, and the default is what people judge a language
by. The proof is the default property; a check at run time is a choice a
build states.prove, verify), keeping assert as
a run time check. assert is the word every reader knows; that the
compiler proves it is what the language adds, not a reason for a second
word.Not decided here: a mark on one claim that it is checked by design, so that
a build at error accepts that one. Nothing needs it yet that the switch does
not cover.
warn. Its manifest says so where it is
read.nikaia check --asserts lists each claim and why it is not proved; it now
prints in check as it did in lower and build.