[fsantanna]

> "part of the goal was to bring synchronous programming to the mainstream"

This was not the original academic goal, but it is now.

We want to offer an imperative alternative to program reactive systems.

[pron]

Any plans on offering formal methods for Céu?

[fsantanna]

Some colleagues are working on an operational semantics of the language (based on the one in the thesis). This will allow us to prove some claims (e.g., reaction termination, bounded memory). Then, we may think about something else. Anything more specific in mind?

[pron]

Temporal logic verification (via model checking, static analysis, test generation, runtime checks etc.)?

[fsantanna]

That would be interesting.

It seems to be feasible given the language semantics.

We'll definitely investigate it.