In order to separate capabilities for compilers, introducing formal verification levels of contracts could be useful. A simple example:
V0: Contracts are only semantically checked.
V1: @require may be compiled into asserts inside of the function. Compile time violations detected through constant folding should not compile.
V2: As V1, but @ensures is also checked.
V3: @require and @ensures are added at the caller side as well. Compile time violations detected through constant folding should not compile.
V4: Detected compile time violations also includes range checks.
V5: Something else
In order to separate capabilities for compilers, introducing formal verification levels of contracts could be useful. A simple example:
V0: Contracts are only semantically checked. V1:
@requiremay be compiled into asserts inside of the function. Compile time violations detected through constant folding should not compile. V2: As V1, but@ensuresis also checked. V3:@requireand@ensuresare added at the caller side as well. Compile time violations detected through constant folding should not compile. V4: Detected compile time violations also includes range checks. V5: Something else