The Coq mailing list

["Perry E. Metzger" <perry AT piermont.com>]

On Mon, 18 Jan 2016 11:11:24 +0100 Chan Ngo 
<chan.ngo2203 AT gmail.com>
wrote:
> > On Jan 5, 2016, at 11:22 AM, Gabriel Scherer
> > <gabriel.scherer AT gmail.com>
> >  wrote:
> > 
> > Note that there has already been work on verifying LLVM passes
> > using a variant of your approach M2:
> > 
> >  Vellmv: Verifying the LLVM
> >  Steve Zdancewic, Dmitri Garbuzov, William Mansky, Vivien Durey,
> > Milo M. K. Martin, Jianzhou Zhao, Santosh Nagarakatte
> >  2012-2015
> >  http://www.cis.upenn.edu/~stevez/vellvm/
> > 
> > This project does not try to generate C++ code, it instead
> > compiles and run the OCaml program extracted from Coq. I think
> > this is a reasonable approach (using either inter-process
> > communication of textual or binary IR representations, or even
> > directly OCaml bindings to the LLVM machinery).
> > 
> 
> Yes, thanks for the pointers. Somehow I already know these
> projects. However, you see that an interface between OCaml code and
> C++ code supported by LLVM is needed.

LLVM is already constructed so that interfaces between passes are
relatively thin and can be written in different languages -- it is
very straightforward to pass the intermediate representation between
them, and there are bindings to the API in languages other than C++.

> In addition, developers cannot employ the full power of LLVM's API
> provided.

LLVM provides OCaml bindings.

> It is interesting and useful if there exists a toolchain that can at
> least provide a way to make specification of LLVM's pass
> implementation in C++ and prove it is correct.

Perhaps, but I will point out that this is a dramatically more
complicated job than doing the work in the way VELLVM does it.

There are good reasons for being able to prove C code directly correct
-- sometimes there's no choice but to use C code, say if it is very
performance critical and/or very low level and/or part of a larger
codebase that is already written in C.

However, the inside of a compiler which has good separation of module
interfaces doesn't seem like such a case, and regardless, a verified
C++ toolchain does not exist and would a vastly more complicated
undertaking than the already difficult verified C toolchain was.

Producing fully verified software artifacts is already a very
difficult job. I think success in such undertakings partially involves
making sure that one tries not to do more than one needs to in order
to get the job done. If you add too much complexity the work will not
terminate, and even if there were a fully verified C++ toolchain it
would not be simple to work with.

The nice part about writing a code pass in Coq and extracting is that
one is not trying to do more than necessary -- it allows one to focus
on mostly the relevant part (the already difficult task of proving an
optimization or the like correct) and not on the complexities of the
semantics of an implementation language like C++.

Perry
-- 
Perry E. Metzger                
perry AT piermont.com