The Coq mailing list

[Larry Lee <llee AT jhsph.edu>]

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 %]