The Coq mailing list

[Larry Lee <llee AT jhsph.edu>]

@Ian. If you're referring to the decision to split Scheme into small and large variants, I understand your frustration. But the decision has certain merits, and should actually simply the proposed project. Scheme has always had a strong following of language researchers and teachers, who have used its simplicity to explore new features and introduce students to functional programming. Language researchers would especially benefit from the development of a Coq model of the language, and R7RS's drive toward simplicity should simplify the proposed project. All in all, I believe that this project would be of benefit to the Scheme community, and would help language researchers, and programmers working on high-reliability applications.

@Ramana. Mind if I study cakeml and use it as a model for the current project?

- Larry

On 04/23/2014 11:38 AM, Ramana Kumar wrote:

Shameless self-promotion of a related project: https://cakeml.org, a formally verified compiler for a (substantial) subset of Standard ML.

On Wed, Apr 23, 2014 at 4:33 PM, J. Ian Johnson <ianj AT ccs.neu.edu> wrote:
You're better off spending your time on a better designed language. I'm not saying this out of spite or bitterness, but out of true concern for your and others' time. Go study the history behind R7RS. No one thinks it's a good idea. Maybe John Cowan, who's only experience in language design is founded solely in toy interpreters.
-Ian

----- Original Message -----
From: llee AT jhsph.edu
To: coq-club AT inria.fr
Sent: Wed, 23 Apr 2014 10:35:08 -0400 (EDT)
Subject: [Coq-Club] Looking For Collaborators to Develop an Open Source Formally Verified Compiler for R7RS Scheme.

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