there are two lines of research I'd take a look at:
1. bidirectional predicates in the Prolog world (I think someone already mentioned logic programming)
2. bidirectional lenses. maybe too domain-specific, but probably a good start:
www.seas.upenn.edu/~harmony/
dl.acm.org/doi/10.1145/...

PLUM folks should be made honorary New Jerseyans...

I see your cinnamon and raise you a cinnamon

thank you!

though to be fair, there is a lot of existing work on reasoning about C programs: softwarefoundations.cis.upenn.edu/vc-current/P...

in the paper, we are using one of them (VST) to reason about C foreign functions linked to CertiCoq-compiled Coq programs.

We didn't go the full ITree route in the paper since the tree is parametrized by a stack of event types, which complicates how the execution function has to be written. (can also have a runtime cost so we have to be careful) But I imagine the ITree approach would organize the proof+program better.

The path is less clear for other effectful programs. There is work on proving effectful programs correct:
* github.com/search?q=rep...
* doi.org/10.4230/LIPI...
* doi.org/10.1145/3293...

Expressing the program with an ITree and writing an execution function for it in C is probably the way to go.

Thank you!

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.

if I misunderstood and you were asking about dynamic checks for safe FFI, there's some work on that too: www.cs.princeton.edu/~appel/paper...

thank you!

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.

i’m prob too old to dare to explain, but in my understanding “cooked” is bad. “cooking” (as in “let him cook”) is good.

though the Twitter Circle was a decent temporary hack for this. I added some of those personal connections to my circle and exclusively tweeted in Turkish there.