Contract language for Catala scopes

[denismerigoux]

Currently, Catala has assertions that let the user specify boolean facts that should hold true when the program runes (else the program crashes). These assertions are actually triple-use : they also stand in as checks of an expected value for test cases, and they are hypothesis that the verification engine can rely on.

It is essential to distinguish the three different uses of current assertions. In particular, testing and verification requires more than assertions, they require a true contract language with preconditions and post-conditions on functions and scopes.

Hence, I propose we add two new keywords to the language, requires and ensures (requiert et garantit). Semantics-wise, these would be syntactic sugars for assertions. But, they could be picked up and receive special treatment by the testing system (@AltGr, @rprimet) or by the verification engine (@R1kM, @pierregoutagny, @rmonat).

What do you think ?

[rmonat]

Following our weekly meeting:

1. assert to raise errors if the condition is not satisfied
2. assume to ensure a given condition is satisfied
3. Maybe a soft_assume for soft constraints? There could also be a need for minimization/maximization of specific variables/datatypes. (Maybe a DSL/config file?)

[R1kM]

For soft constraints, I'd personally be in favor of an external config file, I'm worried that these soft constraints would quickly pollute Catala code. But we should experiment first with the current constraints we'd like to write.

[denismerigoux]

Syntax decision committee :

• requires/nécessite
• ensures/vérifie

We keep assertion