"Perry E. Metzger" <perry@piermont.com> wrote:

> On Fri, 6 Jul 2012 01:42:06 -0400 John Cowan <cowan@mercury.ccil.org>
> wrote:
> > Perry E. Metzger scripsit:
> >
> > > A +1 for switching to an operational semantics. It would be
> > > especially cool to develop an executable semantics...
> >
> > If we are to take the semantics seriously, I think it means
> > developing one whose soundness can be established with a proof
> > assistant.
>
> Agreed. (I had somewhat assumed it, in fact.)

As Eli has correctly pointed out, and some others have already referenced,
there have been significant improvements in the formal semantics world
and in Schemeland particularly that we should take into account. I think
the existing R6RS semantics was done in a way that was compatible with the
Redex system. This is a step forward from what we have now, and while it is
not where I would want to see the semantics of Scheme end, if we are not
going to invest real time into the semantics, then we should at least be
considering using a system that has some level of mechanization in it, and
with Redex we already have most of this work done for us.

That is separate and different than what I hope we will do, which is to
dedicate real effort and real time towards moving forward beyond what we
already have in the Redex R6RS semantics.

--
Aaron W. Hsu | arcfide@sacrideo.us | http://www.sacrideo.us
Programming is just another word for the lost art of thinking.

_______________________________________________
Scheme-reports mailing list
Scheme-reports@scheme-reports.org
http://lists.scheme-reports.org/cgi-bin/mailman/listinfo/scheme-reports