The Coq mailing list

[Ramana Kumar <Ramana.Kumar AT cl.cam.ac.uk>]

I should also mention this other piece of related work: https://www.cl.cam.ac.uk/~mom22/jitawa/.

A verified compiler and runtime for Common Lisp, (as well as a verified theorem prover above it).

(In both CakeML and the above, there is no need to trust extraction.)

A strategy similar to the one outlined by Larry is used. The main possible exception is that in CakeML, for Larry's step (1) we don't verify the implementation of the compiler through the semantics manually (which would be quite painful as Kris pointed out); rather, we use proof-producing synthesis of CakeML code from a definition of the compilation algorithm. In other words, we can reason about functions in the logic that are automatically proved equivalent to the code for the compiler.

On Thu, Apr 24, 2014 at 4:32 PM, Larry Lee <llee AT jhsph.edu> wrote:

Just to clarify. The plan is to translate the semantics given in the R7RS report into a Coq model.This model should be able to evaluate Scheme expressions and in effect behave like an interpreter. After this is done, the plan is to write a compiler in scheme that is R7RS compliant. We can then use the Coq model to (1) verify that this compiler is correct, and (2) run the compiler on itself to compile the compiler. This plan involves verifying that the compiler (written in Scheme) is correct and it also involves verifying the that interpreter (written in Coq) is correct w.r.t the semantics given in the report.

Larry

On 04/24/2014 11:26 AM, Kristopher Micinski wrote:

Sure, but that seems like a smaller code base than trusting the
compiler implemented in scheme is correct without a proof :-)

Kris


On Thu, Apr 24, 2014 at 10:45 AM, Ramana Kumar
<Ramana.Kumar AT cl.cam.ac.uk> wrote:

Regarding extraction: If you extract a Coq definition of compiler to Scheme,
you have to trust that the extracted code has the same semantics as the Coq
definition. I would say this is a significant increase in your trusted code
base from just the Coq kernel (type-checker etc.): you now also trust the
extraction machinery and then whatever you use to run the Scheme.


On Thu, Apr 24, 2014 at 3:09 PM, Kristopher Micinski
<krismicinski AT gmail.com> wrote:

So this will get you an certified interpreter that says "the compiler
is being run correctly."

But that doesn't have any bearing on whether or not the compiler is
*correct*.

It's like writing a compiler in ML and then running it on a verified
runtime, it doesn't give you any hint that your compiler is working
correctly, it just gives you assurance that the compiler isn't being
run in some completely wacky way because the interpreter is wrong.

If you want to prove the compiler is correct, you have to prove it's a
semantics preserving implementation, which is way more involved.

(You could always write parts of the compiler in Coq and then extract
them to Scheme, though...)

Kris


On Thu, Apr 24, 2014 at 9:26 AM, Larry Lee <llee AT jhsph.edu> wrote:

Yeah, It's not trivial. Fortunately, R7RS already possess a formal
semantics
description that we should be able to translate into Coq. Once a Coq
model
is built, we should be able to evaluate and verify Scheme programs. The
plan
is to use the Coq model as an interpreter to "run" the Scheme compiler
on
itself. I'm still recruiting team members, but the idea of building an
interpreter in Coq and a compiler in Scheme, seems (on the surface)
feasible. I downloaded a copy of "CakeML: A Verified Implementation of
ML"
last night and studied the approach that your team used. It looks like
there
may be many useful lessons there.

Larry


On 04/24/2014 02:32 AM, Kristopher Micinski wrote:

Formalizing and implementing verified compilers is a sort of boutique
area that some of the Coq community members are pretty well versed in
(I'm not one of them).

Presumably what you want to do is to model the definition of Scheme
(or whatever) given it's abstract machine formalizations that are (at
this point) folklore.  Then you want to prove the correctness of the
translation in the sense that if you take a program and execute it
using the abstract machine semantics you get an agreement if you
execute the assembly code (or whatever your base is).

One thing that seems suspect is the following: writing the compiler in
Scheme itself doesn't seem trivial.  People usually write the
compilers in Coq so that they can use the facilities of the logic to
argue about the correctness of the compiler.  If you wrote your
compiler in Scheme you'd have to do essentially the same thing, except
a lot more work because you'd have to reason through the embedding of
the semantics.  That seems super nasty.

This is a pretty ambitious open source project, considering that
CakeML is definitely what I'd describe as active research :-)

Kris


On Wed, Apr 23, 2014 at 10:35 AM,  <llee AT jhsph.edu> wrote:

Scheme is a popular dialect of Lisp that posses an elegant syntax and
powerful
semantics.

It's development is directed by a steering committee (the Scheme
Steering
Committee (http://scheme-reports.org/)) that recently released a
document
describing the latest version of the language - R7RS. They are
currently
looking for implementations.

I'm starting a project to create an open-source formally verified
compiler for
Scheme, and am looking for people who are interested in participating.
My
intention is to develop a Coq library that models the new language
standard
and to develop a compiler in Scheme that is formally verified using
this
model. The model itself should be accessible to Scheme developers so
that
it
may be used to verify programs written in Scheme. The compiler should
emphasize reliability and correctness to ensure that it can be used in
high-
reliability applications.

Anyone interested in participating is welcome. I'm looking to assemble
a
small
team to get this project off the ground. If you're interested, please
email
me.

More information about the project can be found here:
https://launchpad.net/willow-r7rs.

Thanks,
- Larry D. Lee jr. [% user.email %]