[Iris-Club] Iris on top of "real-world" languages

[Gregory Malecha]

Thanks everyone from the comments.

Generally, it sounds like there is a great deal of interest in it, but
(currently) not a lot of work except for Robbert's work on C.

As far as automation, it should be possible to re-use a lot of automation
across these languages if we translate to VCs in heap_lang (or another core
language). From Bedrock 1, I would imagine a CPS language (perhaps similar
to what RustBelt did). I imagine that Iris in it's full generality would be
difficulty to automate, but the ability to automate the "boring,
non-concurrent" fragment of imperative programs would have a tremendous
bang-for-the-buck and falling back on MosSel/IPM (which seem pretty good
from my, admittedly limited, uses) for the complex reasoning would be
pretty reasonable in my mind.

@Jesper I agree that the VST folks have done a lot here which is great and
they have developed good automation. My interest in Iris is, to a large
extent, related to its portability. It seems concievable (though not
currently done) that one could do what you suggest and instantiate Iris on
top of Jensen's work and integrate assembly code with C code in a single
logical framework. VST, on the other hand, seems a bit more specialized to
the C operational model. Perhaps you can still do this, and I'd be
interested in work along these lines, but it seems like a bit more of a
leap. As Jeehoon mentioned, weak memory is another feature that Iris
supports (in theory?).

@Robbert, I'd be interested in chatting with you a bit about your work. VST
operates on Clight rather than the full language to avoid the complexities
of evaluation strategies. If you were to plug into CompCert, you could do
something similar. I guess plugging into another compiler would be more
problematic, but it is still the case that Clight programs are also C
programs so you could run your favorite compiler on the Clight code (rather
than the source C). Would making that  simplification make the task easier?

On Thu, Oct 11, 2018, 4:40 AM Robbert Krebbers <mail at robbertkrebbers.nl>
wrote:

> Hi Gregory,
>
> Together with Dan Frumin and Leon Gondelmann at Radboud University
> Nijmegen, I'm working on instantiating Iris with a C language.
> Currently, we are working on automation for non-determinism in
> expressions. In short: we have developed a new version of the logic from
> my POPL'14 paper in Iris that's better suited for automation. On top of
> that new logic, we are building automated tactics (by computational
> reflection) for computing verification conditions automatically.
>
> We eventually would like to support more features of C. First and
> foremost, if we want it to be actually usable, we need support for data
> types (all the different integer types, structs, unions, arrays). Right
> now, we use mathematical integers, and only have limited support for
> arrays (no structs and unions). For this, we could probably learn a lot
> from VST. Apart from that, we would like to support concurrency eventually.
>
> Best,
>
> Robbert
>
> On 10/10/18 10:39 PM, Gregory Malecha wrote:
> > Hello --
> >
> > I'm wondering how much work there has been applying Iris to reason about
> > "real-world" languages. I was really impressed with the RustBelt work,
> > and was wondering if there has been any work applying it to build
> > program logics on top of languages such as C, C++, Rust, or even
> assembly.
> >
> > Any pointers would be greatly appreciated. Even if there isn't any work
> > right now, if there is anyone interested either in producing or
> > consuming this sort of work, it would be great to know about interest.
> >
> > Thank you.
> >
> > --
> > gregory malecha
> > gmalecha.github.io <https://gmalecha.github.io>
> >
>
> --
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20181011/4e4acb12/attachment.html>