We develop an embedded domain specific language inside the dependently typed functional programming language Agda for specifying and verifying properties of functional reactive programs. For this purpose, we embed the temporal logic CTL (computation tree logic) inside dependent type theory.
Our EDSL offers all the standard stream programming primitives, and enriches them with two crucial aspects:
- Side effects. An effectful stream is our model of a reactive program. Upon emission of a value, a side effect may be produced as well. The kind of side effects appears in the type signature, which allows reasoning about determinism of programs.
- Proof terms. We supply primitives and utilities to verify properties of the program, which may depend on both time and side effects.
For example it is possible to verify properties such as:
- Safety properties. "At every point in time, and under any possible side effect or circumstance, a certain proposition is satisfied."
- Liveness properties. "It is always possible to create a side effect such that eventually, a certain proposition will come true."
The diverse properties can be combined into more complex ones, modelling realistic requirements for reactive programs.