On Tue, 22 Apr 2014 10:10:43 -0400 John Cowan <[email protected]> wrote: > Larry Lee scripsit: > > > I'm looking to develop an open-source implementation for R7RS > > that is formally verified. The implementation will be formally > > verified using Coq (http://coq.inria.fr/) and will focus > > initially on the small version of the language. If you are > > interested in assisting with the project, please let me know. > > I can't help with this directly, but I think it has all kinds of > win. What do you intend to use as the implementation language, or > is that still open? >
Generally, if one does formal verification in Coq, one implements in Coq itself, and extracts to another language (Haskell, ML, and Scheme being among the targets Coq supports, although in general OCaml extraction is the best supported.) I find the idea of this being done very appealing. I will note that there isn't a formal semantics currently in existence for R7RS, but that this project would, by its very nature, create such a semantics which could be published as a supplement to the existing report. -- Perry E. Metzger [email protected] _______________________________________________ Scheme-reports mailing list [email protected] http://lists.scheme-reports.org/cgi-bin/mailman/listinfo/scheme-reports
