c3lang
Suggestion: Option to enable some contracts to work in release mode
A suggestion to allow some contracts to be specified to run in release mode, perhaps using an attribute?
This might also be applicable to asserts as well
I will allow it, but it needs to be a concrete proposal how to add it. It's an obvious feature BUT note here that the Rust crate with contracts is not comparable. Most contract plugins will not be able to use static analysis. So unlike the Rust contracts, the C3 contracts are also checked at compile time.
what do you think of an annotation, for example using @nostrip
<*
@require input < 10 @nostrip
*>
fn void do_bar(int input)
{
io::printfn("Doing bar on %d", input);
}
@nostrip
Used for: any declaration
This causes the declaration never to be stripped from the executable, even if it’s not used. This also transitively applies to any dependencies the declaration might have.
I think the problem with contracts as an optimization also contains a fundamental misunderstanding of what contracts are and what they're used for. Contracts enable compile time verification, they only secondarily happen to enable optimizations because it's possible to rule things out.
For example, let's say we have this C code:
c->foo = 123;
if (!c) puts("Hello world");
In this case, is it reasonable to optimize away the if statement? The implicit contract here is that c->foo is crashing on deref anyway, so c can't possibly be NULL. HOWEVER if we're changing c on another thread, it might sometimes give another value! In C, however, it's UB to do so and so the optimization is legal.
What the argument often seems to boil down to is that this optimization should not be allowed just in case. But if we're not allowing it because of the change on another thread, this actually means c can't be loaded into a register and reused either. In fact there are a lot of quite normal optimizations that just fall apart.
So while certainly one should have the ability to turn safety on-off at a more fine grained level, there has to be some sanity and understand of what the contracts actually do.
If we want to make sure that something is ALWAYS checked, why not make it part of the normal code? That seems more logical and doesn't require weird features.
So comparing C3 contracts to Rust's contracts crate is just wrong to begin with. It's an uninformed take. Rust's crate will not do static analysis at compile time to prevent code that violates the contract.
c3c ... -O1 - Safe, high optimization, emit debug info.
So this seems like the answer in most cases, the user can enable compile time safety but still benefit from optimisations if they so choose.
If we go down the rabbit hole of having some contracts enabled, and some disabled in other places, it seems to get confusing quickly. There was a similar situation recently with the accidental pre-pending of * to a require etc, which is not ideal and lead to much confusion
I am not sure. It needs perhaps some sort of proposal on how it should work @always_safe for the module perhaps?
Are you guys discussing design by contracts? I think Ada / SPARK is worth looking into. Probably should not copy what Rust does.
