Language idea: Function contracts about celerity

[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...