[Iris-Club] Using Iris

[Ralf Jung]

Hi Greg,

sorry for the late reply, and I'd be very happy to arrange a video call if you'd
like!  Also see my embedded reply below.

>         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.
> 
> 
>     What about just considering triples of the form { P } c {x. True}? This
>     ensures that c is safe, so I think it suffices for what you want, right?
> 
> This is a good point. I would have thought to use False rather than True in the
> post-condition, is there a reason that you chose False? 

Postcondition "False" would mean that the program never terminates. I don't
think that's what you want? Postcondition "True" is what we use in RustBelt. It
means "the program executes safely and if it terminates, we don't say anything
about the final state".

Notice that Hoare triples are anyway just syntactic sugar, what Iris really is
about is `WP e { v, P }` saying that expression `e` is safe to execute in the
current state and if it terminates, `P` holds for the final state.

For RustBelt, we encoded CPS as a mode of use of the lambda calculus
(continuations are just lambda terms), so things overall work a lot like they do
in the simple language we usually consider in the Iris papers.  In your setting,
is it even possible to talk about what happens when `c` is executed without
specifying a continuation, or is there some syntactic distinction between `c`
and "whole programs" that have an operational semantics?

Kind regards,
Ralf