[Iris-Club] Classical version of Iris?

[Derek Dreyer]

No one is developing a classical version of Iris, so far as I know.  I
don't know if I've ever thought much about what a classical version
would look like, but I imagine that if it makes sense at all, it would
be very painful to work with because you would lose monotonicity.

To answer your question about applicability to Rust, this point about
intuitionistic separation logic not being good for explicit storage
deallocation is an oft-repeated myth.  There is no problem with using
intuitionistic separation logic to reason safely about explicit
deallocation -- the only difficulty is in using it to prove absence of
memory leaks.  Indeed, in classical separation logic, if the
postcondition of your program is "emp", then you know all the memory
has been deallocated, whereas you would not know that in
intuitionistic separation logic since the latter collapses the
distinction between emp and true.  However, even in intuitionistic
separation logic, I believe you can use ghost state to effectively
encode the condition that all memory has been deallocated (e.g. by
starting with some tokens that represent the capability to allocate
memory, and then showing in the postcondition that you have regained
ownership of all of them).  This is maybe more cumbersome but I think
it's doable.

That said, Rust permits memory leaks via reference-counting cycles, so
the point is moot, and I can see no motivation for using classical
rather than intuitionistic separation logic in modeling Rust.

Cheers,
Derek

On Sun, Aug 14, 2016 at 2:08 PM, Jeehoon Kang <jeehoon.kang at sf.snu.ac.kr> wrote:
> Dear Iris Club,
>
> In the ICFP 2016 paper is said "Iris is an intuitionistic separation logic,
> which gives rise to the monotonicity requirement".  I wonder if someone is
> developing a classical version of Iris.
>
> Background: I heard (from some of the Iris authors ;-) that Iris is related
> the RustBelt project which aims to verify "unsafe" Rust programs, which (I
> guess) involves verification of safe memory disposal.  And I just learned
> from a classic textbook (https://www.cs.cmu.edu/~jcr/copenhagen08.pdf) that
> verification of safe memory disposal requires classical separation logic..
>
> Best,
> Jeehoon
>
> PS. Sorry for cluttering everyone's inbox by sending a lot of emails..  I
> will at least try to say something useful.  Thank you for answering all the
> questions!
>
> --
> Jeehoon Kang (Ph.D. student)
> Software Foundations Laboratory
> Seoul National University
>
> --
> iris-club at lists.mpi-sws.org - Mailing List for the Iris Logic
> Management: https://lists.mpi-sws.org/listinfo/iris-club
> Unsubscribe: iris-club-unsubscribe at lists.mpi-sws.org
>