Language idea: Function contracts

[alexrp]

It would be interesting to see if there's something we can do in this space. We have the assert statement currently, but I think there's room for a more principled feature here.

The feature would need to support preconditions and postconditions (with access to the return value). Preconditions would run before any code in the function, while postconditions would need to run after any defer and use statements in the function. Postconditions would only run when an error is not raised from the function.

Compile-time contract checking would be out of scope initially, but could always be done on a best-effort basis later down the line.

I have no idea what the syntax would look like yet.

[alexrp]

One possibility:

contract ::= contract-precondition contract-result-postcondition? contract-error-postcondition? |
             contract-result-postcondition contract-error-postcondition? |
             contract-error-postcondition
contract-precondition ::= 'in' block-expression
contract-result-postcondition ::= 'out' ('as' lower-identifier)? block-expression
contract-error-postcondition ::= 'err' ('as' lower-identifier)? block-expression

contract-statement ::= contract

statement ::= ... |
              contract-statement

Semantics:

• Contracts are only allowed as the first statement in the top-level block of a function declaration (no lambdas).
• Contracts can access the function's parameter bindings.
• Contracts cannot access surrounding local bindings in the function.
• Contracts can mutate the result/error values (e.g. if they have mutable fields). This is unfortunate but would be very hard to prevent. A lint pass could catch obvious cases.
• Contracts cannot ret, raise, or do error-propagating calls.

[alexrp]

It would be better if we could incorporate contracts into function declaration and function type syntax in a similar way to what we did for result type and error type syntax...