Dumb question about contracts: I was reading the docs (
https://c3-lang.org/language-common/contracts/) and this jumped out
"Contracts are optional pre- and post-condition checks that the compiler may use for static analysis, runtime checks and optimization. Note that conforming C3 compilers are not obliged to use pre- and post-conditions at all.
However, violating either pre- or post-conditions is unspecified behaviour, and a compiler may optimize code as if they are always true – even if a potential bug may cause them to be violated.
In safe mode, pre- and post-conditions are checked using runtime asserts."
So I'm probably missing something, but it reads to me like you're adding checks to your code, except there's no guarantee that they will run and whether it's at compile or runtime. And sometimes instead of catching a mistake, these checks will instead silently introduce undefined behaviour into your program. Isn't that kinda bad? How are you supposed to use this stuff reliably?
(otherwise C3 seems really cool!)
"Contracts are optional pre- and post-condition checks that the compiler may use for static analysis, runtime checks and optimization. Note that conforming C3 compilers are not obliged to use pre- and post-conditions at all.
However, violating either pre- or post-conditions is unspecified behaviour, and a compiler may optimize code as if they are always true – even if a potential bug may cause them to be violated.
In safe mode, pre- and post-conditions are checked using runtime asserts."
So I'm probably missing something, but it reads to me like you're adding checks to your code, except there's no guarantee that they will run and whether it's at compile or runtime. And sometimes instead of catching a mistake, these checks will instead silently introduce undefined behaviour into your program. Isn't that kinda bad? How are you supposed to use this stuff reliably?
(otherwise C3 seems really cool!)