The Coq mailing list

["J. Ian Johnson" <ianj AT ccs.neu.edu>]

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