Make assertions explicit in the syntax

[Schaeff]

We currently allow statements of the form

a + b == 43

Which are interpreted as assertions, which need to hold at run time.

To be more explicit, introduce a reserved keyword assert which needs to wrap these statements.

assert(a + b == 43)

Implementation

While the current parsing of conditions is custom, with such a keyword we could implement it as

def assert(bool b) -> (field)

We can then parse statements which are a single function call foo as

foo(a, b, c)
Statement::Assertion(Expression::FunctionCall("foo", vec![...]))

And enforce some rules during semantic checking:

• Assertion statements must contain a call to assert with a boolean expression as argument
• assert must not be called outside of Statement::Assertion

Thus, only assert(bool) would make it through semantic checking and can be handled as TypedStatement::Assertion(BooleanExpression) after that.

This is merely a suggestion, though!

[GuthL]

I do not see the use for such modification. The current implementation allows to write constraint in a pretty natural way. I just see this proposal as an overhead at this point.

[GuthL]

After discussing with @Schaeff, I think you are right. Having an assert will allow the clear separation between Constraint and Boolean. Functions should be able to return Bool and Assert should enforce Constraint.