Your code compiles, so **your example is invalid**.
nim c test_assert2.nim
Hint: used config file
'/Users/user/.choosenim/toolchains/nim-0.19.6/config/nim.cfg' [Conf]
Hint: system [Processing]
Hint: test_assert2 [Processing]
CC: test_assert2
CC: stdlib_system
Hint: [Link]
Hint: operation successful (12403 lines compiled; 0.535 sec total;
16.359MiB peakmem; Debug Build) [SuccessX]
Run
To work the same way as `gnatprove`, **the compiler / prover / whatever must
fail**.
I repeat what I said before: it's bad, **very** bad, if the plane software
discovers mid-air that an assertion fails. It's much better to discover **at
compile time** that a contract is not satisfied.
