Formal methods with stateful functions

[simondlevy]

This is more of a general question than a Copilot issue, but I thought that sharing it with the Copilot community could be helpful for others too.

I am finding Copilot's support for stateful functions extremely useful in implementing nontrivial models like PID control in a very elegant way, but I am wondering how the introduction of state to otherwise pure functions will affect our ability to apply formal methods and reasoning to Copilot-based software. Because Copilot was designed with formal methods in mind, I am sure that the use of stateful function doesn't introduce the kind of intractability that you get with procedural / object-oriented languages (Python, Java, C++, ...); however, I was unable to find any publications or other formal analysis of the issue. My tentative guess would be that tying state to streams is what allows Copilot to avoid these problems, but I would be grateful for any comments or links that the community can provide.

[ivanperez-keera]

My tentative guess would be that tying state to streams is what allows Copilot to avoid these problems, but I would be grateful for any comments or links that the community can provide.

This is indeed the case.

State is available in the ability to access the past via delays. This is common in temporal frameworks like stream programming, and it's also how things work in reactive programming and in Functional Reactive Programming.

Copilot provides several mechanisms that leverage formal reasoning applied to streams. For starters, there's the library copilot-theorem, that allows you to use SMT-solvers and model checkers (beware of #495 which needs to be fixed) to prove properties of streams.

Papers that talk about this include: https://link.springer.com/chapter/10.1007/978-3-319-23820-3_6. The documentation at https://github.com/Copilot-Language/copilot/tree/master/copilot-theorem is a bit outdated, but there are references at: https://github.com/Copilot-Language/copilot/tree/master/copilot-theorem#references.

We also have a library, copilot-verifier (https://github.com/Copilot-Language/copilot-verifier) that formally verifies that the output C code matches the original spec precisely. This is a great exercise in verification of stateful code, since the ring-buffers used to keep information about streams are where state is kept.

The paper to consult on the verifier is: https://dl.acm.org/doi/abs/10.1145/3607841.

There's lots of publications on co-induction (streams are coinductive datatypes) and formal verification in e.g., agda, coq, idris, etc. So there's no fear that the introduction of state via streams is somehow limiting the formality of the language or the correctness of the specifications. These are well understood results.

[ivanperez-keera]

And just for general education, reactive languages have to limit the access to the past (and the future), to ensure that programs run efficiently and do not have time leaks or require unbounded memory.

FRP frameworks, for example, provide a limited number of ways to access the past. Yampa provides a large collection of combinators that are stateful, as well as explicit state-carrying signal functions (loop and loopPre). Dunai provides feedback as well as others that also depend on the past in multiple ways. Copilot achieves this via a combination of two things: delays (which provide access to the past) and recursion (which provide access to oneself); by combining these two, a stream can access its own past, or become stateful, without losing any formality.

[simondlevy]

Thank you for this very thorough explanation, Ivan. I am working my way through the "Assuring the Guardians" paper and meanwhile will close this issue.

[ivanperez-keera]

Sounds great. Always a pleasure. Keep us posted.

I'd been keep to see both what you can prove about your properties/streams, and what you cannot prove (but would like to). That could create opportunities both for communicating how useful this can be, and for improving it.