The Coq mailing list

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

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