<div dir="ltr"><div dir="ltr">Hello --<div><br></div><div>I'm interested in using Iris in a large (industry) development and I have a few questions about it to see if it is something that would work for us. Two questions come to mind right now, but more will probably come up as I dig deeper.</div><div><br></div><div>1/ All of the resources that I have seen have applied Iris to Hoare triples. Has anyone tried applying it to Hoare doubles, i.e. `{ P } c` means that `P` guarantees that `c` is safe (but says nothing about a final state). I thought that the RustBelt work might have done something like this since the paper talks about how the logic is applied to a CPS language but I didn't find anything in that development.</div><div><br></div><div>2/ One of the things that I need to track in the development is interactions with the outside world (for our project, this is hardware like ethernet nics). Right now, I'm thinking that a nice way to do this would be through a pre-condition that states what traces are possible when running the program. Essentially, I want to add a spatial predicate `TRACE p` such that `{ TRACE p } c` means that the only interaction that `c` can do is to follow the protocol defined by `p` which is morally something akin to `trace -> Prop`. My intuition suggests that this should be fairly simple in Iris if I model it as a module that carries around the trace behind an abstract predicate. The difficulty is that I need to ensure totality, mainly that I have to follow the protocol, i.e. I can't diverge. Normally, this would just require a total Hoare logic, but if my protocol is infinite, things become a little more complex. Has anyone done something like this before? Is there anything that I should be weary of?</div><div><br></div><div>I'd be interested in chatting more with anyone if they have an hour or so, I am in Boston and have a relatively flexible schedule to accommodate other time zones.</div><div><br></div><div>Thanks for any feedback.</div><div><div><br></div>-- <br><div dir="ltr" class="m_2294560266436205366gmail_signature"><div dir="ltr"><div><div dir="ltr"><div>gregory malecha</div><div><a href="https://gmalecha.github.io" target="_blank">gmalecha.github.io</a></div></div></div></div></div></div></div></div>