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

[Robbert Krebbers]

On 10/11/18 9:29 PM, Gregory Malecha wrote:
> @Robbert, I'd be interested in chatting with you a bit about your 
> work.
That certainly would be possible, I'll mail you in private about that.

> 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?
The primary motivation of our work is indeed that the verification is 
sound w.r.t. any compiler; not just CompCert.

As you said, one could translate each C program into a version in which 
all sequencing has been made explicit, and then use that program for 
both the verification and as the input of your favorite C compiler. I 
don't find this satisfactory. In the end of the day, it would be much 
nicer if one could verify C programs as if, without having to modify the 
source code of the program.

Besides, a program logic as the one we develop for C in Iris cannot just 
be used for proving properties of concrete programs, but it can also be 
used (typically by building logical relations) for different purposes, e.g.:

- Proving correctness of program transformations
- Proving correctness of say static analyses

In both of these cases you cannot modify the source programs.

Robbert