The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

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