"A Verified Foreign Function Interface between Coq and C", by me, Kathrin Stark and Andrew W. Appel will appear at POPL 2025! https://www.cs.princeton.edu/~appel/papers/VeriFFI.pdf
this is the culmination of years of research (and most of my grad school work), so I'm excited to see it finally published! 🎉
this is the culmination of years of research (and most of my grad school work), so I'm excited to see it finally published! 🎉
Comments
I don't foresee a huge challenge for the mutable array example: We have a purely functional model that computes the same result; VST is good at such proofs. We also now have proofs about how the GC deals with mutation.
* https://github.com/search?q=repo%3APrincetonUniversity%2FVST%20itree&type=code
* https://doi.org/10.4230/LIPIcs.ITP.2021.32
* https://doi.org/10.1145/3293880.329410
Expressing the program with an ITree and writing an execution function for it in C is probably the way to go.
could this approach inspire a framework for runtime checks of dynamically changing models?
can you clarify what you mean by dynamically changing models? do you mean based on input from the outside world? I think you would have to model that as an effect, like in section 12.2.